Nuprl - Pf term_types

PrintForm Definitions mb automata 3 Sections GenAutomata Doc

t:Term, ds,da,de:Top. term_types(ds;da;de;(t)') ~ term_types(ds;da;de;t)

By: Analyze 0 THEN Unfolds [`term_types`;`addprime`] 0 THEN TermInd 1 THEN Reduce 0 THEN All (Folds [`term_types`;`addprime`]) THEN Try (Complete Auto) THEN Try (UnivCD THEN Analyze THEN BackThruSomeHyp)

Generated subgoals:

None

About:

PrintForm Definitions mb automata 3 Sections GenAutomata Doc