At:
term subst2 addprime11
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
5.
as: (LabelTerm) List
6.
v:Label. (v [x2]) (v 1of(unzip(as)))
apply_alist(as;x2;x2') = apply_alist(as;x2;x2)
By:
Unfold `apply_alist` 0
THEN
Unfold `find` 0
THEN
ListInd -2
THEN
Reduce 0
THEN
Try ((Unfold `unzip` 0) THEN (Reduce 0) THEN (InstHyp [x2] -1) THEN (Try (RWW "member_singleton" 0)) THEN (Try ((Unfold `l_member` -1) THEN (Reduce -1) THEN ExRepD)))
THEN
Try
((((Reduce 0) THEN SplitOnConclITE THEN (Reduce 0) THEN (Try BackThruSomeHyp) THEN (InstHyp [v@0] -7)) THEN (RWW "cons_member" -1) THEN (Analyze -1))
THEN
(Try
(((Analyze -4) THEN (RWW "member_singleton" -2))
THEN
(BackThru
Thm*l1,l2:Label. l1 = l2 l1 = l2)
THEN
RelRST))
THEN
(Try ((Unfold `unzip` 0) THEN (Reduce 0) THEN Trivial)))
Generated subgoals:
Type{i'}
as:(Label
Term) List.
(
term_vars(x)) 
(v 
apply_alist(as;x2;x2') = apply_alist(as;x2;x2)
l2 
