DEFINITION pr2_gen_cabbr()
TYPE =
∀c:C
.∀t1:T
.∀t2:T
.pr2 c t1 t2
→∀e:C
.∀u:T
.∀d:nat
.getl d c (CHead e (Bind Abbr) u)
→∀a0:C
.csubst1 d u c a0
→∀a:C
.drop (S O) d a0 a
→∀x1:T.(subst1 d u t1 (lift (S O) d x1))→(ex2 T λx2:T.subst1 d u t2 (lift (S O) d x2) λx2:T.pr2 a x1 x2)
BODY =
assume c: C
assume t1: T
assume t2: T
suppose H: pr2 c t1 t2
we proceed by induction on H to prove
∀e:C
.∀u:T
.∀d:nat
.getl d c (CHead e (Bind Abbr) u)
→∀a0:C
.csubst1 d u c a0
→∀a:C
.drop (S O) d a0 a
→∀x1:T.(subst1 d u t1 (lift (S O) d x1))→(ex2 T λx2:T.subst1 d u t2 (lift (S O) d x2) λx2:T.pr2 a x1 x2)
case pr2_free : c0:C t3:T t4:T H0:pr0 t3 t4 ⇒
the thesis becomes
∀e:C
.∀u:T
.∀d:nat
.getl d c0 (CHead e (Bind Abbr) u)
→∀a0:C
.csubst1 d u c0 a0
→∀a:C
.drop (S O) d a0 a
→∀x1:T.∀H4:(subst1 d u t3 (lift (S O) d x1)).(ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr2 a x1 x2)
assume e: C
assume u: T
assume d: nat
suppose : getl d c0 (CHead e (Bind Abbr) u)
assume a0: C
suppose : csubst1 d u c0 a0
assume a: C
suppose : drop (S O) d a0 a
assume x1: T
suppose H4: subst1 d u t3 (lift (S O) d x1)
by (pr0_refl .)
we proved pr0 u u
by (pr0_subst1 . . H0 . . . H4 . previous)
we proved ex2 T λw2:T.pr0 (lift (S O) d x1) w2 λw2:T.subst1 d u t4 w2
we proceed by induction on the previous result to prove ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr2 a x1 x2
case ex_intro2 : x:T H5:pr0 (lift (S O) d x1) x H6:subst1 d u t4 x ⇒
the thesis becomes ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr2 a x1 x2
by (pr0_gen_lift . . . . H5)
we proved ex2 T λt2:T.eq T x (lift (S O) d t2) λt2:T.pr0 x1 t2
we proceed by induction on the previous result to prove ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr2 a x1 x2
case ex_intro2 : x0:T H7:eq T x (lift (S O) d x0) H8:pr0 x1 x0 ⇒
the thesis becomes ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr2 a x1 x2
(H9)
we proceed by induction on H7 to prove subst1 d u t4 (lift (S O) d x0)
case refl_equal : ⇒
the thesis becomes the hypothesis H6
subst1 d u t4 (lift (S O) d x0)
end of H9
by (pr2_free . . . H8)
we proved pr2 a x1 x0
by (ex_intro2 . . . . H9 previous)
ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr2 a x1 x2
ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr2 a x1 x2
we proved ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr2 a x1 x2
∀e:C
.∀u:T
.∀d:nat
.getl d c0 (CHead e (Bind Abbr) u)
→∀a0:C
.csubst1 d u c0 a0
→∀a:C
.drop (S O) d a0 a
→∀x1:T.∀H4:(subst1 d u t3 (lift (S O) d x1)).(ex2 T λx2:T.subst1 d u t4 (lift (S O) d x2) λx2:T.pr2 a x1 x2)
case pr2_delta : c0:C d:C u:T i:nat H0:getl i c0 (CHead d (Bind Abbr) u) t3:T t4:T H1:pr0 t3 t4 t:T H2:subst0 i u t4 t ⇒
the thesis becomes
∀e:C
.∀u0:T
.∀d0:nat
.∀H3:getl d0 c0 (CHead e (Bind Abbr) u0)
.∀a0:C
.∀H4:csubst1 d0 u0 c0 a0
.∀a:C
.∀H5:(drop (S O) d0 a0 a).∀x1:T.∀H6:(subst1 d0 u0 t3 (lift (S O) d0 x1)).(ex2 T λx2:T.subst1 d0 u0 t (lift (S O) d0 x2) λx2:T.pr2 a x1 x2)
assume e: C
assume u0: T
assume d0: nat
suppose H3: getl d0 c0 (CHead e (Bind Abbr) u0)
assume a0: C
suppose H4: csubst1 d0 u0 c0 a0
assume a: C
suppose H5: drop (S O) d0 a0 a
assume x1: T
suppose H6: subst1 d0 u0 t3 (lift (S O) d0 x1)
by (pr0_refl .)
we proved pr0 u0 u0
by (pr0_subst1 . . H1 . . . H6 . previous)
we proved ex2 T λw2:T.pr0 (lift (S O) d0 x1) w2 λw2:T.subst1 d0 u0 t4 w2
we proceed by induction on the previous result to prove ex2 T λx2:T.subst1 d0 u0 t (lift (S O) d0 x2) λx2:T.pr2 a x1 x2
case ex_intro2 : x:T H7:pr0 (lift (S O) d0 x1) x H8:subst1 d0 u0 t4 x ⇒
the thesis becomes ex2 T λx2:T.subst1 d0 u0 t (lift (S O) d0 x2) λx2:T.pr2 a x1 x2
by (pr0_gen_lift . . . . H7)
we proved ex2 T λt2:T.eq T x (lift (S O) d0 t2) λt2:T.pr0 x1 t2
we proceed by induction on the previous result to prove ex2 T λx2:T.subst1 d0 u0 t (lift (S O) d0 x2) λx2:T.pr2 a x1 x2
case ex_intro2 : x0:T H9:eq T x (lift (S O) d0 x0) H10:pr0 x1 x0 ⇒
the thesis becomes ex2 T λx2:T.subst1 d0 u0 t (lift (S O) d0 x2) λx2:T.pr2 a x1 x2
(H11)
we proceed by induction on H9 to prove subst1 d0 u0 t4 (lift (S O) d0 x0)
case refl_equal : ⇒
the thesis becomes the hypothesis H8
subst1 d0 u0 t4 (lift (S O) d0 x0)
end of H11
(h1)
suppose H12: lt i d0
(h1)
by (subst1_single . . . . H2)
subst1 i u t4 t
end of h1
(h2)
by (lt_neq . . H12)
not (eq nat i d0)
end of h2
by (subst1_confluence_neq . . . . h1 . . . H11 h2)
we proved ex2 T λt:T.subst1 d0 u0 t t λt:T.subst1 i u (lift (S O) d0 x0) t
we proceed by induction on the previous result to prove ex2 T λx2:T.subst1 d0 u0 t (lift (S O) d0 x2) λx2:T.pr2 a x1 x2
case ex_intro2 : x2:T H13:subst1 d0 u0 t x2 H14:subst1 i u (lift (S O) d0 x0) x2 ⇒
the thesis becomes ex2 T λx3:T.subst1 d0 u0 t (lift (S O) d0 x3) λx3:T.pr2 a x1 x3
by (csubst1_getl_lt . . H12 . . . H4 . H0)
we proved ex2 C λe2:C.csubst1 (minus d0 i) u0 (CHead d (Bind Abbr) u) e2 λe2:C.getl i a0 e2
we proceed by induction on the previous result to prove ex2 T λx3:T.subst1 d0 u0 t (lift (S O) d0 x3) λx3:T.pr2 a x1 x3
case ex_intro2 : x3:C H15:csubst1 (minus d0 i) u0 (CHead d (Bind Abbr) u) x3 H16:getl i a0 x3 ⇒
the thesis becomes ex2 T λx4:T.subst1 d0 u0 t (lift (S O) d0 x4) λx4:T.pr2 a x1 x4
(H17)
by (minus_x_Sy . . H12)
we proved eq nat (minus d0 i) (S (minus d0 (S i)))
we proceed by induction on the previous result to prove csubst1 (S (minus d0 (S i))) u0 (CHead d (Bind Abbr) u) x3
case refl_equal : ⇒
the thesis becomes the hypothesis H15
csubst1 (S (minus d0 (S i))) u0 (CHead d (Bind Abbr) u) x3
end of H17
(H18)
consider H17
we proved csubst1 (S (minus d0 (S i))) u0 (CHead d (Bind Abbr) u) x3
that is equivalent to csubst1 (s (Bind Abbr) (minus d0 (S i))) u0 (CHead d (Bind Abbr) u) x3
by (csubst1_gen_head . . . . . . previous)
ex3_2
T
C
λu2:T.λc2:C.eq C x3 (CHead c2 (Bind Abbr) u2)
λu2:T.λ:C.subst1 (minus d0 (S i)) u0 u u2
λ:T.λc2:C.csubst1 (minus d0 (S i)) u0 d c2
end of H18
we proceed by induction on H18 to prove ex2 T λx4:T.subst1 d0 u0 t (lift (S O) d0 x4) λx4:T.pr2 a x1 x4
case ex3_2_intro : x4:T x5:C H19:eq C x3 (CHead x5 (Bind Abbr) x4) H20:subst1 (minus d0 (S i)) u0 u x4 :csubst1 (minus d0 (S i)) u0 d x5 ⇒
the thesis becomes ex2 T λx6:T.subst1 d0 u0 t (lift (S O) d0 x6) λx6:T.pr2 a x1 x6
(H22)
we proceed by induction on H19 to prove getl i a0 (CHead x5 (Bind Abbr) x4)
case refl_equal : ⇒
the thesis becomes the hypothesis H16
getl i a0 (CHead x5 (Bind Abbr) x4)
end of H22
(H23)
by (lt_plus_minus . . H12)
we proved eq nat d0 (S (plus i (minus d0 (S i))))
we proceed by induction on the previous result to prove drop (S O) (S (plus i (minus d0 (S i)))) a0 a
case refl_equal : ⇒
the thesis becomes the hypothesis H5
drop (S O) (S (plus i (minus d0 (S i)))) a0 a
end of H23
by (getl_drop_conf_lt . . . . . H22 . . . H23)
we proved
ex3_2
T
C
λv:T.λ:C.eq T x4 (lift (S O) (minus d0 (S i)) v)
λv:T.λe0:C.getl i a (CHead e0 (Bind Abbr) v)
λ:T.λe0:C.drop (S O) (minus d0 (S i)) x5 e0
we proceed by induction on the previous result to prove ex2 T λx6:T.subst1 d0 u0 t (lift (S O) d0 x6) λx6:T.pr2 a x1 x6
case ex3_2_intro : x6:T x7:C H24:eq T x4 (lift (S O) (minus d0 (S i)) x6) H25:getl i a (CHead x7 (Bind Abbr) x6) :drop (S O) (minus d0 (S i)) x5 x7 ⇒
the thesis becomes ex2 T λx8:T.subst1 d0 u0 t (lift (S O) d0 x8) λx8:T.pr2 a x1 x8
(H27)
we proceed by induction on H24 to prove subst1 (minus d0 (S i)) u0 u (lift (S O) (minus d0 (S i)) x6)
case refl_equal : ⇒
the thesis becomes the hypothesis H20
subst1 (minus d0 (S i)) u0 u (lift (S O) (minus d0 (S i)) x6)
end of H27
by (subst1_subst1_back . . . . H14 . . . H27)
we proved
ex2
T
λt:T.subst1 i (lift (S O) (minus d0 (S i)) x6) (lift (S O) d0 x0) t
λt:T.subst1 (S (plus (minus d0 (S i)) i)) u0 x2 t
we proceed by induction on the previous result to prove ex2 T λx8:T.subst1 d0 u0 t (lift (S O) d0 x8) λx8:T.pr2 a x1 x8
case ex_intro2 : x8:T H28:subst1 i (lift (S O) (minus d0 (S i)) x6) (lift (S O) d0 x0) x8 H29:subst1 (S (plus (minus d0 (S i)) i)) u0 x2 x8 ⇒
the thesis becomes ex2 T λx9:T.subst1 d0 u0 t (lift (S O) d0 x9) λx9:T.pr2 a x1 x9
(H30)
by (lt_plus_minus . . H12)
we proved eq nat d0 (S (plus i (minus d0 (S i))))
we proceed by induction on the previous result to prove
subst1
i
lift (S O) (minus d0 (S i)) x6
lift (S O) (S (plus i (minus d0 (S i)))) x0
x8
case refl_equal : ⇒
the thesis becomes the hypothesis H28
subst1
i
lift (S O) (minus d0 (S i)) x6
lift (S O) (S (plus i (minus d0 (S i)))) x0
x8
end of H30
by (subst1_gen_lift_lt . . . . . . H30)
we proved ex2 T λt2:T.eq T x8 (lift (S O) (S (plus i (minus d0 (S i)))) t2) λt2:T.subst1 i x6 x0 t2
we proceed by induction on the previous result to prove ex2 T λx9:T.subst1 d0 u0 t (lift (S O) d0 x9) λx9:T.pr2 a x1 x9
case ex_intro2 : x9:T H31:eq T x8 (lift (S O) (S (plus i (minus d0 (S i)))) x9) H32:subst1 i x6 x0 x9 ⇒
the thesis becomes ex2 T λx10:T.subst1 d0 u0 t (lift (S O) d0 x10) λx10:T.pr2 a x1 x10
(H33)
we proceed by induction on H31 to prove
subst1
S (plus (minus d0 (S i)) i)
u0
x2
lift (S O) (S (plus i (minus d0 (S i)))) x9
case refl_equal : ⇒
the thesis becomes the hypothesis H29
subst1
S (plus (minus d0 (S i)) i)
u0
x2
lift (S O) (S (plus i (minus d0 (S i)))) x9
end of H33
(H34)
by (lt_plus_minus . . H12)
we proved eq nat d0 (S (plus i (minus d0 (S i))))
by (eq_ind_r . . . H33 . previous)
subst1 (S (plus (minus d0 (S i)) i)) u0 x2 (lift (S O) d0 x9)
end of H34
(H35)
by (lt_plus_minus_r . . H12)
we proved eq nat d0 (S (plus (minus d0 (S i)) i))
by (eq_ind_r . . . H34 . previous)
subst1 d0 u0 x2 (lift (S O) d0 x9)
end of H35
(h1)
by (subst1_trans . . . . H13 . H35)
subst1 d0 u0 t (lift (S O) d0 x9)
end of h1
(h2) by (pr2_delta1 . . . . H25 . . H10 . H32) we proved pr2 a x1 x9
by (ex_intro2 . . . . h1 h2)
ex2 T λx10:T.subst1 d0 u0 t (lift (S O) d0 x10) λx10:T.pr2 a x1 x10
ex2 T λx9:T.subst1 d0 u0 t (lift (S O) d0 x9) λx9:T.pr2 a x1 x9
ex2 T λx8:T.subst1 d0 u0 t (lift (S O) d0 x8) λx8:T.pr2 a x1 x8
ex2 T λx6:T.subst1 d0 u0 t (lift (S O) d0 x6) λx6:T.pr2 a x1 x6
ex2 T λx4:T.subst1 d0 u0 t (lift (S O) d0 x4) λx4:T.pr2 a x1 x4
ex2 T λx3:T.subst1 d0 u0 t (lift (S O) d0 x3) λx3:T.pr2 a x1 x3
we proved ex2 T λx2:T.subst1 d0 u0 t (lift (S O) d0 x2) λx2:T.pr2 a x1 x2
(lt i d0)→(ex2 T λx2:T.subst1 d0 u0 t (lift (S O) d0 x2) λx2:T.pr2 a x1 x2)
end of h1
(h2)
suppose H12: eq nat i d0
(H13)
by (eq_ind_r . . . H11 . H12)
subst1 i u0 t4 (lift (S O) i x0)
end of H13
(H15)
by (eq_ind_r . . . H4 . H12)
csubst1 i u0 c0 a0
end of H15
(H16)
by (eq_ind_r . . . H3 . H12)
getl i c0 (CHead e (Bind Abbr) u0)
end of H16
we proceed by induction on H12 to prove ex2 T λx2:T.subst1 d0 u0 t (lift (S O) d0 x2) λx2:T.pr2 a x1 x2
case refl_equal : ⇒
the thesis becomes ex2 T λx2:T.subst1 i u0 t (lift (S O) i x2) λx2:T.pr2 a x1 x2
(H17)
by (getl_mono . . . H0 . H16)
we proved eq C (CHead d (Bind Abbr) u) (CHead e (Bind Abbr) u0)
we proceed by induction on the previous result to prove getl i c0 (CHead e (Bind Abbr) u0)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
getl i c0 (CHead e (Bind Abbr) u0)
end of H17
(H18)
by (getl_mono . . . H0 . H16)
we proved eq C (CHead d (Bind Abbr) u) (CHead e (Bind Abbr) u0)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c1 ⇒c1
<λ:C.C> CASE CHead e (Bind Abbr) u0 OF CSort ⇒d | CHead c1 ⇒c1
eq
C
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c1 ⇒c1 (CHead d (Bind Abbr) u)
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒d | CHead c1 ⇒c1 (CHead e (Bind Abbr) u0)
end of H18
(h1)
(H19)
by (getl_mono . . . H0 . H16)
we proved eq C (CHead d (Bind Abbr) u) (CHead e (Bind Abbr) u0)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t0⇒t0
<λ:C.T> CASE CHead e (Bind Abbr) u0 OF CSort ⇒u | CHead t0⇒t0
eq
T
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t0⇒t0 (CHead d (Bind Abbr) u)
λe0:C.<λ:C.T> CASE e0 OF CSort ⇒u | CHead t0⇒t0 (CHead e (Bind Abbr) u0)
end of H19
suppose H20: eq C d e
(H21)
consider H19
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t0⇒t0
<λ:C.T> CASE CHead e (Bind Abbr) u0 OF CSort ⇒u | CHead t0⇒t0
that is equivalent to eq T u u0
by (eq_ind_r . . . H17 . previous)
getl i c0 (CHead e (Bind Abbr) u)
end of H21
(H22)
consider H19
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t0⇒t0
<λ:C.T> CASE CHead e (Bind Abbr) u0 OF CSort ⇒u | CHead t0⇒t0
that is equivalent to eq T u u0
by (eq_ind_r . . . H13 . previous)
subst1 i u t4 (lift (S O) i x0)
end of H22
consider H19
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t0⇒t0
<λ:C.T> CASE CHead e (Bind Abbr) u0 OF CSort ⇒u | CHead t0⇒t0
that is equivalent to eq T u u0
we proceed by induction on the previous result to prove ex2 T λx2:T.subst1 i u0 t (lift (S O) i x2) λx2:T.pr2 a x1 x2
case refl_equal : ⇒
the thesis becomes ex2 T λx2:T.subst1 i u t (lift (S O) i x2) λx2:T.pr2 a x1 x2
by (subst1_single . . . . H2)
we proved subst1 i u t4 t
by (subst1_confluence_eq . . . . previous . H22)
we proved ex2 T λt:T.subst1 i u t t λt:T.subst1 i u (lift (S O) i x0) t
we proceed by induction on the previous result to prove ex2 T λx2:T.subst1 i u t (lift (S O) i x2) λx2:T.pr2 a x1 x2
case ex_intro2 : x2:T H25:subst1 i u t x2 H26:subst1 i u (lift (S O) i x0) x2 ⇒
the thesis becomes ex2 T λx3:T.subst1 i u t (lift (S O) i x3) λx3:T.pr2 a x1 x3
(H27)
(h1) by (le_n .) we proved le i i
(h2)
(h1)
by (le_n .)
we proved le (plus (S O) i) (plus (S O) i)
lt i (plus (S O) i)
end of h1
(h2)
by (plus_sym . .)
eq nat (plus i (S O)) (plus (S O) i)
end of h2
by (eq_ind_r . . . h1 . h2)
lt i (plus i (S O))
end of h2
by (subst1_gen_lift_eq . . . . . . h1 h2 H26)
we proved eq T x2 (lift (S O) i x0)
we proceed by induction on the previous result to prove subst1 i u t (lift (S O) i x0)
case refl_equal : ⇒
the thesis becomes the hypothesis H25
subst1 i u t (lift (S O) i x0)
end of H27
by (pr2_free . . . H10)
we proved pr2 a x1 x0
by (ex_intro2 . . . . H27 previous)
ex2 T λx3:T.subst1 i u t (lift (S O) i x3) λx3:T.pr2 a x1 x3
ex2 T λx2:T.subst1 i u t (lift (S O) i x2) λx2:T.pr2 a x1 x2
we proved ex2 T λx2:T.subst1 i u0 t (lift (S O) i x2) λx2:T.pr2 a x1 x2
(eq C d e)→(ex2 T λx2:T.subst1 i u0 t (lift (S O) i x2) λx2:T.pr2 a x1 x2)
end of h1
(h2)
consider H18
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c1 ⇒c1
<λ:C.C> CASE CHead e (Bind Abbr) u0 OF CSort ⇒d | CHead c1 ⇒c1
eq C d e
end of h2
by (h1 h2)
ex2 T λx2:T.subst1 i u0 t (lift (S O) i x2) λx2:T.pr2 a x1 x2
we proved ex2 T λx2:T.subst1 d0 u0 t (lift (S O) d0 x2) λx2:T.pr2 a x1 x2
(eq nat i d0)→(ex2 T λx2:T.subst1 d0 u0 t (lift (S O) d0 x2) λx2:T.pr2 a x1 x2)
end of h2
(h3)
suppose H12: lt d0 i
(h1)
by (subst1_single . . . . H2)
subst1 i u t4 t
end of h1
(h2)
by (lt_neq . . H12)
we proved not (eq nat d0 i)
by (sym_not_eq . . . previous)
not (eq nat i d0)
end of h2
by (subst1_confluence_neq . . . . h1 . . . H11 h2)
we proved ex2 T λt:T.subst1 d0 u0 t t λt:T.subst1 i u (lift (S O) d0 x0) t
we proceed by induction on the previous result to prove ex2 T λx2:T.subst1 d0 u0 t (lift (S O) d0 x2) λx2:T.pr2 a x1 x2
case ex_intro2 : x2:T H13:subst1 d0 u0 t x2 H14:subst1 i u (lift (S O) d0 x0) x2 ⇒
the thesis becomes ex2 T λx3:T.subst1 d0 u0 t (lift (S O) d0 x3) λx3:T.pr2 a x1 x3
(h1)
consider H12
we proved lt d0 i
le (plus (S O) d0) i
end of h1
(h2)
by (plus_sym . .)
eq nat (plus d0 (S O)) (plus (S O) d0)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved le (plus d0 (S O)) i
by (subst1_gen_lift_ge . . . . . . H14 previous)
we proved ex2 T λt2:T.eq T x2 (lift (S O) d0 t2) λt2:T.subst1 (minus i (S O)) u x0 t2
we proceed by induction on the previous result to prove ex2 T λx3:T.subst1 d0 u0 t (lift (S O) d0 x3) λx3:T.pr2 a x1 x3
case ex_intro2 : x3:T H15:eq T x2 (lift (S O) d0 x3) H16:subst1 (minus i (S O)) u x0 x3 ⇒
the thesis becomes ex2 T λx4:T.subst1 d0 u0 t (lift (S O) d0 x4) λx4:T.pr2 a x1 x4
(H17)
we proceed by induction on H15 to prove subst1 d0 u0 t (lift (S O) d0 x3)
case refl_equal : ⇒
the thesis becomes the hypothesis H13
subst1 d0 u0 t (lift (S O) d0 x3)
end of H17
(h1)
consider H12
we proved lt d0 i
that is equivalent to le (S d0) i
by (le_S . . previous)
we proved le (S d0) (S i)
by (le_S_n . . previous)
we proved le d0 i
by (csubst1_getl_ge . . previous . . . H4 . H0)
getl i a0 (CHead d (Bind Abbr) u)
end of h1
(h2)
(h1)
consider H12
we proved lt d0 i
le (plus (S O) d0) i
end of h1
(h2)
by (plus_sym . .)
eq nat (plus d0 (S O)) (plus (S O) d0)
end of h2
by (eq_ind_r . . . h1 . h2)
le (plus d0 (S O)) i
end of h2
by (getl_drop_conf_ge . . . h1 . . . H5 h2)
we proved getl (minus i (S O)) a (CHead d (Bind Abbr) u)
by (pr2_delta1 . . . . previous . . H10 . H16)
we proved pr2 a x1 x3
by (ex_intro2 . . . . H17 previous)
ex2 T λx4:T.subst1 d0 u0 t (lift (S O) d0 x4) λx4:T.pr2 a x1 x4
ex2 T λx3:T.subst1 d0 u0 t (lift (S O) d0 x3) λx3:T.pr2 a x1 x3
we proved ex2 T λx2:T.subst1 d0 u0 t (lift (S O) d0 x2) λx2:T.pr2 a x1 x2
(lt d0 i)→(ex2 T λx2:T.subst1 d0 u0 t (lift (S O) d0 x2) λx2:T.pr2 a x1 x2)
end of h3
by (lt_eq_gt_e . . . h1 h2 h3)
ex2 T λx2:T.subst1 d0 u0 t (lift (S O) d0 x2) λx2:T.pr2 a x1 x2
ex2 T λx2:T.subst1 d0 u0 t (lift (S O) d0 x2) λx2:T.pr2 a x1 x2
we proved ex2 T λx2:T.subst1 d0 u0 t (lift (S O) d0 x2) λx2:T.pr2 a x1 x2
∀e:C
.∀u0:T
.∀d0:nat
.∀H3:getl d0 c0 (CHead e (Bind Abbr) u0)
.∀a0:C
.∀H4:csubst1 d0 u0 c0 a0
.∀a:C
.∀H5:(drop (S O) d0 a0 a).∀x1:T.∀H6:(subst1 d0 u0 t3 (lift (S O) d0 x1)).(ex2 T λx2:T.subst1 d0 u0 t (lift (S O) d0 x2) λx2:T.pr2 a x1 x2)
we proved
∀e:C
.∀u:T
.∀d:nat
.getl d c (CHead e (Bind Abbr) u)
→∀a0:C
.csubst1 d u c a0
→∀a:C
.drop (S O) d a0 a
→∀x1:T.(subst1 d u t1 (lift (S O) d x1))→(ex2 T λx2:T.subst1 d u t2 (lift (S O) d x2) λx2:T.pr2 a x1 x2)
we proved
∀c:C
.∀t1:T
.∀t2:T
.pr2 c t1 t2
→∀e:C
.∀u:T
.∀d:nat
.getl d c (CHead e (Bind Abbr) u)
→∀a0:C
.csubst1 d u c a0
→∀a:C
.drop (S O) d a0 a
→∀x1:T.(subst1 d u t1 (lift (S O) d x1))→(ex2 T λx2:T.subst1 d u t2 (lift (S O) d x2) λx2:T.pr2 a x1 x2)