Nuprl - Proof: gro eacc wf

For any graph t:GraphObject(the_graph), T:Type. t.eacc (TVT)TVT

By: Auto THEN MoveToConcl -1 THEN RepeatFor 6 (Analyze -1) THEN Unfold `gro_eacc` 0 THEN Reduce 0 THEN Analyze 0 THEN AllHyps (h.IsectHD T h)

Generated subgoals:

None

About: