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

At: trivial term subst 1 2 2
1. t: Term
2. u: TermType{i'}
3. w: t:{v:Term| u(v) }as:(LabelTerm) List. (x:Label. unprime(apply_alist(as;x;x)) = x) unprime(term_subst(as;t)) = unprime(t)
4. x: Label
5. as: (LabelTerm) List
6. x:Label. unprime(apply_alist(as;x;x)) = x
7. unprime(apply_alist(as;x;x)) = x
8. (x 1of(unzip(as)))

unprime(apply_alist(as;x;x')) = unprime(x')
By: RWW "apply_alist_non_member" 0
Generated subgoals:

None

About:
productlistsetapplyfunctionuniverseequalimpliesall

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