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

At: rel subst2 addprime 1 1 2 1
1. r: rel()
2. as: (LabelTerm) List
3. 1of(unzip(as)) = rel_vars(r)

||map(t.term_subst2(as;(t)');r.args)|| = ||map(t.term_subst(as;t);r.args)||
By: RWW "map_length_nat" 0
Generated subgoals:

None

About:
productlistintlambdaequal

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