Nuprl - Proof: gro vacc wf

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

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

Generated subgoals:

None

About: