(2steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

At: rel vars addprime 1
1. r: rel()

reduce(t,vs. term_primed_vars(t) @ vs;nil;map(t.(t)';r.args)) = reduce(t,vs. term_vars(t) @ vs;nil;r.args)
By:
Analyze 1
THEN
ListInd 2
THEN
All Reduce
THEN
Try (Complete Auto)
THEN
Try Analyze
THEN
Try ((Inst Thm* t:Term. term_primed_vars((t)') ~ term_vars(t) [u]) THEN (HypSubst -1 0))
Generated subgoals:

None

About:
listnillambdaequal

(2steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc