Nuprl - Pf term subst2 addprime

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

x:Term, as:(LabelTerm) List. (v:Label. (v term_vars(x)) (v 1of(unzip(as)))) term_subst2(as;(x)') = term_subst(as;x)

By: Analyze 0 THEN Unfolds [`term_subst`;`term_subst2`;`addprime`] 0 THEN TermInd 1 THEN Reduce 0 THEN Try (Complete Auto) THEN All (Folds [`term_subst`;`term_subst2`;`addprime`]) THEN Try (Auto THEN Analyze THEN BackThruSomeHyp THEN (RWW "member_append" -1) THEN BackThruSomeHyp THEN TrivialOr)

Generated subgoal:

1 1. x: Term
2. u: TermType{i'}
3. w: x:{v:Term| u(v) }as:(LabelTerm) List. (v:Label. (v term_vars(x)) (v 1of(unzip(as)))) term_subst2(as;(x)') = term_subst(as;x)
4. x2: Label
as:(LabelTerm) List. (v:Label. (v [x2]) (v 1of(unzip(as)))) apply_alist(as;x2;x2') = apply_alist(as;x2;x2)

About:

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