PrintForm Definitions mb automata 2 Sections GenAutomata Doc

At: term free vars addprime


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:
sqequalall

PrintForm Definitions mb automata 2 Sections GenAutomata Doc