Nuprl - Pf term eq wf

a,b:Term. term_eq(a;b)

By: Analyze 0 THEN TermInd -1 THEN Analyze 0 THEN TermInd -1 THEN RecUnfold `term_eq` 0 THEN Reduce 0 THEN BackThruSomeHyp

Generated subgoals:

None

About: