FDL
>
PVS
>
Graphs
>
subgraphs
>
subgraph
vert
sub
>
pf:subgraph
vert
sub
>
1
> 1
(6 nodes)
Conclusion
-1.
subset?
(V!1, vert(G!1))
1. {i | vert(G!1)(i)
AND
V!1(i)}
=
V!1
Tactic
APPLY-EXTENSIONALITY 1 HIDE? T
Premise 1.
(has
proof
of 5 steps)
-1.
subset?
(V!1, vert(G!1))
1. (vert(G!1)(x!1)
AND
V!1(x!1))
=
V!1(x!1)
