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

At: rel primed vars rel vars 1 2 1 1
1. name: relname()
2. r1: Term List
3. x: Label
4. u: Term
5. v: Term List
6. (x reduce(t,vs. term_primed_vars(t) @ vs;nil;v)) (x reduce(t,vs. term_vars(t) @ vs;nil;v))
7. (x term_primed_vars(u))

(x term_vars(u))
By: BackThru Thm* x:Label, u:Term. (x term_primed_vars(u)) (x term_vars(u))
Generated subgoals:

None

About:
listnillambdaimplies

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