Nuprl - Proof: decidable equal gr v

For any graph the_obj:GraphObject(the_graph), x,y:V. Dec(x = y)

By: Auto THEN Inst Thm* graphobj-properties [the_graph;the_obj] THEN Analyze -1 THEN RW (SweepUpC (RevHypC -2)) 0

Generated subgoals:

None

About: