Nuprl - Proof: graph-isomorphic weakening 1

1. G: Graph
2. H: Graph
3. G = H

H H

By: Unfold `graph-isomorphic` 0 THEN InstConcl [Id;Id] THEN Reduce 0 THEN Try (BackThru Thm* Bij(T; T; Id))

Generated subgoal:

1 (Id,Id) o Incidence(H) = Incidence(H) o Id Edges(H)Vertices(H)Vertices(H) 1 step

About: