DEFINITION pr3_subst1()
TYPE =
∀c:C
.∀e:C
.∀v:T
.∀i:nat
.getl i c (CHead e (Bind Abbr) v)
→∀t1:T.∀t2:T.(pr3 c t1 t2)→∀w1:T.(subst1 i v t1 w1)→(ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t2 w2)
BODY =
assume c: C
assume e: C
assume v: T
assume i: nat
suppose H: getl i c (CHead e (Bind Abbr) v)
assume t1: T
assume t2: T
suppose H0: pr3 c t1 t2
we proceed by induction on H0 to prove ∀w1:T.(subst1 i v t1 w1)→(ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t2 w2)
case pr3_refl : t:T ⇒
the thesis becomes ∀w1:T.∀H1:(subst1 i v t w1).(ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t w2)
assume w1: T
suppose H1: subst1 i v t w1
by (pr3_refl . .)
we proved pr3 c w1 w1
by (ex_intro2 . . . . previous H1)
we proved ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t w2
∀w1:T.∀H1:(subst1 i v t w1).(ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t w2)
case pr3_sing : t3:T t4:T H1:pr2 c t4 t3 t5:T :pr3 c t3 t5 ⇒
the thesis becomes ∀w1:T.∀H4:(subst1 i v t4 w1).(ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t5 w2)
(H3) by induction hypothesis we know ∀w1:T.(subst1 i v t3 w1)→(ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t5 w2)
assume w1: T
suppose H4: subst1 i v t4 w1
by (pr2_subst1 . . . . H . . H1 . H4)
we proved ex2 T λw2:T.pr2 c w1 w2 λw2:T.subst1 i v t3 w2
we proceed by induction on the previous result to prove ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t5 w2
case ex_intro2 : x:T H5:pr2 c w1 x H6:subst1 i v t3 x ⇒
the thesis becomes ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t5 w2
by (H3 . H6)
we proved ex2 T λw2:T.pr3 c x w2 λw2:T.subst1 i v t5 w2
we proceed by induction on the previous result to prove ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t5 w2
case ex_intro2 : x0:T H7:pr3 c x x0 H8:subst1 i v t5 x0 ⇒
the thesis becomes ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t5 w2
by (pr3_sing . . . H5 . H7)
we proved pr3 c w1 x0
by (ex_intro2 . . . . previous H8)
ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t5 w2
ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t5 w2
we proved ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t5 w2
∀w1:T.∀H4:(subst1 i v t4 w1).(ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t5 w2)
we proved ∀w1:T.(subst1 i v t1 w1)→(ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t2 w2)
we proved
∀c:C
.∀e:C
.∀v:T
.∀i:nat
.getl i c (CHead e (Bind Abbr) v)
→∀t1:T.∀t2:T.(pr3 c t1 t2)→∀w1:T.(subst1 i v t1 w1)→(ex2 T λw2:T.pr3 c w1 w2 λw2:T.subst1 i v t2 w2)