Nuprl - Pf trivial_term_subst 1

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

At: trivial term subst 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

unprime(apply_alist(as;x;x')) = unprime(x')

By: InstHyp [x] -1 THEN Assert ((x 1of(unzip(as))) (x 1of(unzip(as))))

Generated subgoals:

1 7. unprime(apply_alist(as;x;x)) = x
(x 1of(unzip(as))) (x 1of(unzip(as)))

2 7. unprime(apply_alist(as;x;x)) = x
8. (x 1of(unzip(as))) (x 1of(unzip(as)))
unprime(apply_alist(as;x;x')) = unprime(x')

About:

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