Nuprl - Pf trivial_term_subst 1 1

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

At: trivial term subst 1 1

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

(x 1of(unzip(as))) (x 1of(unzip(as)))

By: Fold `decidable` 0 THEN BackThru Thm* x:T, l:T List. (y:T. Dec(x = y)) Dec((x l)) THEN Easy

Generated subgoals:

None

About:

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