Nuprl - Pf term free vars addprime

PrintForm Definitions mb automata 2 Sections GenAutomata Doc

t:Term. term_free_vars((t)') ~ term_free_vars(t)

By: Analyze 0 THEN Unfolds [`term_free_vars`;`addprime`] 0 THEN TermInd 1 THEN Reduce 0 THEN Try Trivial THEN All (Folds [`addprime`;`term_free_vars`]) THEN Try (Analyze THEN BackThruSomeHyp)

Generated subgoals:

None

About:

PrintForm Definitions mb automata 2 Sections GenAutomata Doc