Nuprl - Pf term vars addprime

PrintForm Definitions mb automata 2 Sections GenAutomata Doc

t:Term. term_primed_vars((t)') ~ term_vars(t)

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

Generated subgoals:

None

About:

PrintForm Definitions mb automata 2 Sections GenAutomata Doc