Nuprl - Pf vc concl wf

PrintForm Definitions mb automata 2 Sections GenAutomata Doc

At: vc concl wf

v:vc{i:l}(). vc_concl(v) Fmla

By: Auto THEN Unfold `vc_concl` 0 THEN Analyze 1 THEN Reduce 0

Generated subgoals:

None

About:

PrintForm Definitions mb automata 2 Sections GenAutomata Doc