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

At: rel subst2 addprime 1 1 2
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: BackThru Thm* a,b:T List. ||a|| = ||b|| (i:. i < ||a|| a[i] = b[i]) a = b
Generated subgoals:

1 ||map(t.term_subst2(as;(t)');r.args)|| = ||map(t.term_subst(as;t);r.args)||
2 i:. i < ||map(t.term_subst2(as;(t)');r.args)|| map(t.term_subst2(as;(t)');r.args)[i] = map(t.term_subst(as;t);r.args)[i]

About:
productlistintless_thanlambdaequalimpliesall

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