Nuprl - Pf termlist eq wf

a,b:Term List. termlist_eq(a;b)

By: Analyze 0 THEN ListInd -1 THEN Analyze 0 THEN ListInd -1 THEN RecUnfold `termlist_eq` 0 THEN Reduce 0 THEN BackThruSomeHyp

Generated subgoals:

None

About: