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

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

(t.term_subst2(as;t)) o (t.(t)') = (t.term_subst2(as;(t)')) TermTerm
By:
Ext
THEN
Reduce 0
Generated subgoals:

None

About:
productlistlambdafunctionequal

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