DEFINITION ty3_gen_cvoid()
TYPE =
∀g:G
.∀c:C
.∀t1:T
.∀t2:T
.ty3 g c t1 t2
→∀e:C
.∀u:T
.∀d:nat
.getl d c (CHead e (Bind Void) u)
→∀a:C
.drop (S O) d c a
→ex3_2 T T λy1:T.λ:T.eq T t1 (lift (S O) d y1) λ:T.λy2:T.eq T t2 (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
BODY =
assume g: G
assume c: C
assume t1: T
assume t2: T
suppose H: ty3 g c t1 t2
we proceed by induction on H to prove
∀e:C
.∀u:T
.∀d:nat
.getl d c (CHead e (Bind Void) u)
→∀a:C
.drop (S O) d c a
→ex3_2 T T λy1:T.λ:T.eq T t1 (lift (S O) d y1) λ:T.λy2:T.eq T t2 (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
case ty3_conv : c0:C t3:T t:T H0:ty3 g c0 t3 t u:T t4:T H2:ty3 g c0 u t4 H4:pc3 c0 t4 t3 ⇒
the thesis becomes
∀e:C
.∀u0:T
.∀d:nat
.∀H5:getl d c0 (CHead e (Bind Void) u0)
.∀a:C
.∀H6:drop (S O) d c0 a
.ex3_2 T T λy1:T.λ:T.eq T u (lift (S O) d y1) λ:T.λy2:T.eq T t3 (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
(H1) by induction hypothesis we know
∀e:C
.∀u:T
.∀d:nat
.getl d c0 (CHead e (Bind Void) u)
→∀a:C
.drop (S O) d c0 a
→ex3_2 T T λy1:T.λ:T.eq T t3 (lift (S O) d y1) λ:T.λy2:T.eq T t (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
(H3) by induction hypothesis we know
∀e:C
.∀u0:T
.∀d:nat
.getl d c0 (CHead e (Bind Void) u0)
→∀a:C
.drop (S O) d c0 a
→ex3_2 T T λy1:T.λ:T.eq T u (lift (S O) d y1) λ:T.λy2:T.eq T t4 (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
assume e: C
assume u0: T
assume d: nat
suppose H5: getl d c0 (CHead e (Bind Void) u0)
assume a: C
suppose H6: drop (S O) d c0 a
(H7)
by (H3 . . . H5 . H6)
ex3_2 T T λy1:T.λ:T.eq T u (lift (S O) d y1) λ:T.λy2:T.eq T t4 (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
end of H7
we proceed by induction on H7 to prove
ex3_2 T T λy1:T.λ:T.eq T u (lift (S O) d y1) λ:T.λy2:T.eq T t3 (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
case ex3_2_intro : x0:T x1:T H8:eq T u (lift (S O) d x0) H9:eq T t4 (lift (S O) d x1) H10:ty3 g a x0 x1 ⇒
the thesis becomes
ex3_2 T T λy1:T.λ:T.eq T u (lift (S O) d y1) λ:T.λy2:T.eq T t3 (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
(H11)
we proceed by induction on H9 to prove pc3 c0 (lift (S O) d x1) t3
case refl_equal : ⇒
the thesis becomes the hypothesis H4
pc3 c0 (lift (S O) d x1) t3
end of H11
(H12)
we proceed by induction on H9 to prove ty3 g c0 u (lift (S O) d x1)
case refl_equal : ⇒
the thesis becomes the hypothesis H2
ty3 g c0 u (lift (S O) d x1)
end of H12
(H14)
by (H1 . . . H5 . H6)
ex3_2 T T λy1:T.λ:T.eq T t3 (lift (S O) d y1) λ:T.λy2:T.eq T t (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
end of H14
we proceed by induction on H14 to prove
ex3_2
T
T
λy1:T.λ:T.eq T (lift (S O) d x0) (lift (S O) d y1)
λ:T.λy2:T.eq T t3 (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
case ex3_2_intro : x2:T x3:T H15:eq T t3 (lift (S O) d x2) H16:eq T t (lift (S O) d x3) H17:ty3 g a x2 x3 ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.eq T (lift (S O) d x0) (lift (S O) d y1)
λ:T.λy2:T.eq T t3 (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
(H18)
we proceed by induction on H16 to prove ty3 g c0 t3 (lift (S O) d x3)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
ty3 g c0 t3 (lift (S O) d x3)
end of H18
(H20)
we proceed by induction on H15 to prove pc3 c0 (lift (S O) d x1) (lift (S O) d x2)
case refl_equal : ⇒
the thesis becomes the hypothesis H11
pc3 c0 (lift (S O) d x1) (lift (S O) d x2)
end of H20
(h1)
by (refl_equal . .)
eq T (lift (S O) d x0) (lift (S O) d x0)
end of h1
(h2)
by (refl_equal . .)
eq T (lift (S O) d x2) (lift (S O) d x2)
end of h2
(h3)
by (pc3_gen_lift . . . . . H20 . H6)
we proved pc3 a x1 x2
by (ty3_conv . . . . H17 . . H10 previous)
ty3 g a x0 x2
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
we proved
ex3_2
T
T
λy1:T.λ:T.eq T (lift (S O) d x0) (lift (S O) d y1)
λ:T.λy2:T.eq T (lift (S O) d x2) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
by (eq_ind_r . . . previous . H15)
ex3_2
T
T
λy1:T.λ:T.eq T (lift (S O) d x0) (lift (S O) d y1)
λ:T.λy2:T.eq T t3 (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
we proved
ex3_2
T
T
λy1:T.λ:T.eq T (lift (S O) d x0) (lift (S O) d y1)
λ:T.λy2:T.eq T t3 (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
by (eq_ind_r . . . previous . H8)
ex3_2 T T λy1:T.λ:T.eq T u (lift (S O) d y1) λ:T.λy2:T.eq T t3 (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
we proved
ex3_2 T T λy1:T.λ:T.eq T u (lift (S O) d y1) λ:T.λy2:T.eq T t3 (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
∀e:C
.∀u0:T
.∀d:nat
.∀H5:getl d c0 (CHead e (Bind Void) u0)
.∀a:C
.∀H6:drop (S O) d c0 a
.ex3_2 T T λy1:T.λ:T.eq T u (lift (S O) d y1) λ:T.λy2:T.eq T t3 (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
case ty3_sort : c0:C m:nat ⇒
the thesis becomes
∀e:C
.∀u:T
.∀d:nat
.getl d c0 (CHead e (Bind Void) u)
→∀a:C
.drop (S O) d c0 a
→(ex3_2
T
T
λy1:T.λ:T.eq T (TSort m) (lift (S O) d y1)
λ:T.λy2:T.eq T (TSort (next g m)) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2)
assume e: C
assume u: T
assume d: nat
suppose : getl d c0 (CHead e (Bind Void) u)
assume a: C
suppose : drop (S O) d c0 a
(h1)
(h1)
by (refl_equal . .)
eq T (TSort m) (TSort m)
end of h1
(h2)
by (lift_sort . . .)
eq T (lift (S O) d (TSort m)) (TSort m)
end of h2
by (eq_ind_r . . . h1 . h2)
eq T (TSort m) (lift (S O) d (TSort m))
end of h1
(h2)
(h1)
by (refl_equal . .)
eq T (TSort (next g m)) (TSort (next g m))
end of h1
(h2)
by (lift_sort . . .)
eq T (lift (S O) d (TSort (next g m))) (TSort (next g m))
end of h2
by (eq_ind_r . . . h1 . h2)
eq T (TSort (next g m)) (lift (S O) d (TSort (next g m)))
end of h2
(h3)
by (ty3_sort . . .)
ty3 g a (TSort m) (TSort (next g m))
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
we proved
ex3_2
T
T
λy1:T.λ:T.eq T (TSort m) (lift (S O) d y1)
λ:T.λy2:T.eq T (TSort (next g m)) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
∀e:C
.∀u:T
.∀d:nat
.getl d c0 (CHead e (Bind Void) u)
→∀a:C
.drop (S O) d c0 a
→(ex3_2
T
T
λy1:T.λ:T.eq T (TSort m) (lift (S O) d y1)
λ:T.λy2:T.eq T (TSort (next g m)) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2)
case ty3_abbr : n:nat c0:C d:C u:T H0:getl n c0 (CHead d (Bind Abbr) u) t:T H1:ty3 g d u t ⇒
the thesis becomes
∀e:C
.∀u0:T
.∀d0:nat
.∀H3:getl d0 c0 (CHead e (Bind Void) u0)
.∀a:C
.∀H4:drop (S O) d0 c0 a
.ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
(H2) by induction hypothesis we know
∀e:C
.∀u0:T
.∀d0:nat
.getl d0 d (CHead e (Bind Void) u0)
→∀a:C
.drop (S O) d0 d a
→ex3_2 T T λy1:T.λ:T.eq T u (lift (S O) d0 y1) λ:T.λy2:T.eq T t (lift (S O) d0 y2) λy1:T.λy2:T.ty3 g a y1 y2
assume e: C
assume u0: T
assume d0: nat
suppose H3: getl d0 c0 (CHead e (Bind Void) u0)
assume a: C
suppose H4: drop (S O) d0 c0 a
(h1)
suppose H5: lt n d0
(H6)
by (minus_x_Sy . . H5)
we proved eq nat (minus d0 n) (S (minus d0 (S n)))
we proceed by induction on the previous result to prove
getl
S (minus d0 (S n))
CHead d (Bind Abbr) u
CHead e (Bind Void) u0
case refl_equal : ⇒
the thesis becomes
getl
minus d0 n
CHead d (Bind Abbr) u
CHead e (Bind Void) u0
consider H5
we proved lt n d0
that is equivalent to le (S n) d0
by (le_S . . previous)
we proved le (S n) (S d0)
by (le_S_n . . previous)
we proved le n d0
by (getl_conf_le . . . H3 . . H0 previous)
getl
minus d0 n
CHead d (Bind Abbr) u
CHead e (Bind Void) u0
getl
S (minus d0 (S n))
CHead d (Bind Abbr) u
CHead e (Bind Void) u0
end of H6
(H7)
by (lt_plus_minus . . H5)
we proved eq nat d0 (S (plus n (minus d0 (S n))))
we proceed by induction on the previous result to prove drop (S O) (S (plus n (minus d0 (S n)))) c0 a
case refl_equal : ⇒
the thesis becomes the hypothesis H4
drop (S O) (S (plus n (minus d0 (S n)))) c0 a
end of H7
by (getl_drop_conf_lt . . . . . H0 . . . H7)
we proved
ex3_2
T
C
λv:T.λ:C.eq T u (lift (S O) (minus d0 (S n)) v)
λv:T.λe0:C.getl n a (CHead e0 (Bind Abbr) v)
λ:T.λe0:C.drop (S O) (minus d0 (S n)) d e0
we proceed by induction on the previous result to prove
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
case ex3_2_intro : x0:T x1:C H8:eq T u (lift (S O) (minus d0 (S n)) x0) H9:getl n a (CHead x1 (Bind Abbr) x0) H10:drop (S O) (minus d0 (S n)) d x1 ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
(H11)
we proceed by induction on H8 to prove
∀e0:C
.∀u1:T
.∀d1:nat
.getl d1 d (CHead e0 (Bind Void) u1)
→∀a0:C
.drop (S O) d1 d a0
→(ex3_2
T
T
λy1:T.λ:T.eq T (lift (S O) (minus d0 (S n)) x0) (lift (S O) d1 y1)
λ:T.λy2:T.eq T t (lift (S O) d1 y2)
λy1:T.λy2:T.ty3 g a0 y1 y2)
case refl_equal : ⇒
the thesis becomes the hypothesis H2
∀e0:C
.∀u1:T
.∀d1:nat
.getl d1 d (CHead e0 (Bind Void) u1)
→∀a0:C
.drop (S O) d1 d a0
→(ex3_2
T
T
λy1:T.λ:T.eq T (lift (S O) (minus d0 (S n)) x0) (lift (S O) d1 y1)
λ:T.λy2:T.eq T t (lift (S O) d1 y2)
λy1:T.λy2:T.ty3 g a0 y1 y2)
end of H11
(H12)
we proceed by induction on H8 to prove ty3 g d (lift (S O) (minus d0 (S n)) x0) t
case refl_equal : ⇒
the thesis becomes the hypothesis H1
ty3 g d (lift (S O) (minus d0 (S n)) x0) t
end of H12
(H13)
by (getl_gen_S . . . . . H6)
we proved
getl
r (Bind Abbr) (minus d0 (S n))
d
CHead e (Bind Void) u0
that is equivalent to getl (minus d0 (S n)) d (CHead e (Bind Void) u0)
by (H11 . . . previous . H10)
ex3_2
T
T
λy1:T
.λ:T
.eq
T
lift (S O) (minus d0 (S n)) x0
lift (S O) (minus d0 (S n)) y1
λ:T.λy2:T.eq T t (lift (S O) (minus d0 (S n)) y2)
λy1:T.λy2:T.ty3 g x1 y1 y2
end of H13
we proceed by induction on H13 to prove
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
case ex3_2_intro : x2:T x3:T H14:eq T (lift (S O) (minus d0 (S n)) x0) (lift (S O) (minus d0 (S n)) x2) H15:eq T t (lift (S O) (minus d0 (S n)) x3) H16:ty3 g x1 x2 x3 ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
(H18)
by (lift_inj . . . . H14)
we proved eq T x0 x2
by (eq_ind_r . . . H16 . previous)
ty3 g x1 x0 x3
end of H18
by (le_O_n .)
we proved le O (minus d0 (S n))
by (lift_d . . . . . previous)
we proved
eq
T
lift (S O) (plus (S n) (minus d0 (S n))) (lift (S n) O x3)
lift (S n) O (lift (S O) (minus d0 (S n)) x3)
we proceed by induction on the previous result to prove
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T
.λy2:T
.eq
T
lift (S n) O (lift (S O) (minus d0 (S n)) x3)
lift (S O) d0 y2
λy1:T.λy2:T.ty3 g a y1 y2
case refl_equal : ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T
.λy2:T
.eq
T
lift (S O) (plus (S n) (minus d0 (S n))) (lift (S n) O x3)
lift (S O) d0 y2
λy1:T.λy2:T.ty3 g a y1 y2
consider H5
we proved lt n d0
that is equivalent to le (S n) d0
by (le_plus_minus . . previous)
we proved eq nat d0 (plus (S n) (minus d0 (S n)))
we proceed by induction on the previous result to prove
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T
.λy2:T
.eq
T
lift (S O) (plus (S n) (minus d0 (S n))) (lift (S n) O x3)
lift (S O) d0 y2
λy1:T.λy2:T.ty3 g a y1 y2
case refl_equal : ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S O) d0 (lift (S n) O x3)) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
(h1)
(h1)
by (refl_equal . .)
eq T (TLRef n) (TLRef n)
end of h1
(h2)
by (lift_lref_lt . . . H5)
eq T (lift (S O) d0 (TLRef n)) (TLRef n)
end of h2
by (eq_ind_r . . . h1 . h2)
eq T (TLRef n) (lift (S O) d0 (TLRef n))
end of h1
(h2)
by (refl_equal . .)
eq
T
lift (S O) d0 (lift (S n) O x3)
lift (S O) d0 (lift (S n) O x3)
end of h2
(h3)
by (ty3_abbr . . . . . H9 . H18)
ty3 g a (TLRef n) (lift (S n) O x3)
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S O) d0 (lift (S n) O x3)) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T
.λy2:T
.eq
T
lift (S O) (plus (S n) (minus d0 (S n))) (lift (S n) O x3)
lift (S O) d0 y2
λy1:T.λy2:T.ty3 g a y1 y2
we proved
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T
.λy2:T
.eq
T
lift (S n) O (lift (S O) (minus d0 (S n)) x3)
lift (S O) d0 y2
λy1:T.λy2:T.ty3 g a y1 y2
by (eq_ind_r . . . previous . H15)
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
we proved
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
lt n d0
→(ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2)
end of h1
(h2)
suppose H5: eq nat n d0
(H7)
by (eq_ind_r . . . H3 . H5)
getl n c0 (CHead e (Bind Void) u0)
end of H7
we proceed by induction on H5 to prove
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
case refl_equal : ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) n y1)
λ:T.λy2:T.eq T (lift (S n) O t) (lift (S O) n y2)
λy1:T.λy2:T.ty3 g a y1 y2
(H9)
by (getl_mono . . . H0 . H7)
we proved eq C (CHead d (Bind Abbr) u) (CHead e (Bind Void) u0)
we proceed by induction on the previous result to prove
<λ:C.Prop>
CASE CHead e (Bind Void) u0 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:C.Prop>
CASE CHead d (Bind Abbr) u OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
consider I
we proved True
<λ:C.Prop>
CASE CHead d (Bind Abbr) u OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
<λ:C.Prop>
CASE CHead e (Bind Void) u0 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
end of H9
consider H9
we proved
<λ:C.Prop>
CASE CHead e (Bind Void) u0 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒True | Abst⇒False | Void⇒False
| Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) n y1)
λ:T.λy2:T.eq T (lift (S n) O t) (lift (S O) n y2)
λy1:T.λy2:T.ty3 g a y1 y2
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) n y1)
λ:T.λy2:T.eq T (lift (S n) O t) (lift (S O) n y2)
λy1:T.λy2:T.ty3 g a y1 y2
we proved
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
eq nat n d0
→(ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2)
end of h2
(h3)
suppose H5: lt d0 n
(h1)
by (refl_equal . .)
we proved
eq
nat
S (plus O (minus n (S O)))
S (plus O (minus n (S O)))
that is equivalent to
eq
nat
plus (S O) (minus n (S O))
S (plus O (minus n (S O)))
we proceed by induction on the previous result to prove
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef (S (plus O (minus n (S O))))) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
case refl_equal : ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef (plus (S O) (minus n (S O)))) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
(h1)
(h1)
(h1)
by (refl_equal . .)
eq
T
TLRef (plus (minus n (S O)) (S O))
TLRef (plus (minus n (S O)) (S O))
end of h1
(h2)
by (lt_le_minus . . H5)
we proved le d0 (minus n (S O))
by (lift_lref_ge . . . previous)
eq
T
lift (S O) d0 (TLRef (minus n (S O)))
TLRef (plus (minus n (S O)) (S O))
end of h2
by (eq_ind_r . . . h1 . h2)
eq
T
TLRef (plus (minus n (S O)) (S O))
lift (S O) d0 (TLRef (minus n (S O)))
end of h1
(h2)
(h1)
by (refl_equal . .)
we proved eq T (lift (S n) O t) (lift (S n) O t)
eq T (lift (S n) O t) (lift (plus (S O) n) O t)
end of h1
(h2)
(h1)
consider H5
we proved lt d0 n
that is equivalent to le (S d0) (plus O n)
by (le_S . . previous)
we proved le (S d0) (S (plus O n))
by (le_S_n . . previous)
le d0 (plus O n)
end of h1
(h2) by (le_O_n .) we proved le O d0
by (lift_free . . . . . h1 h2)
eq T (lift (S O) d0 (lift n O t)) (lift (plus (S O) n) O t)
end of h2
by (eq_ind_r . . . h1 . h2)
eq T (lift (S n) O t) (lift (S O) d0 (lift n O t))
end of h2
(h3)
(h1)
(h1)
consider H5
we proved lt d0 n
le (plus (S O) d0) n
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)) n
by (getl_drop_conf_ge . . . H0 . . . H4 previous)
we proved getl (minus n (S O)) a (CHead d (Bind Abbr) u)
by (ty3_abbr . . . . . previous . H1)
ty3 g a (TLRef (minus n (S O))) (lift (S (minus n (S O))) O t)
end of h1
(h2)
by (le_O_n .)
we proved le O d0
by (le_lt_trans . . . previous H5)
we proved lt O n
by (minus_x_SO . previous)
eq nat n (S (minus n (S O)))
end of h2
by (eq_ind_r . . . h1 . h2)
ty3 g a (TLRef (minus n (S O))) (lift n O t)
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef (plus (minus n (S O)) (S O))) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
end of h1
(h2)
by (plus_sym . .)
eq
nat
plus (S O) (minus n (S O))
plus (minus n (S O)) (S O)
end of h2
by (eq_ind_r . . . h1 . h2)
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef (plus (S O) (minus n (S O)))) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef (S (plus O (minus n (S O))))) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
end of h1
(h2)
by (le_O_n .)
we proved le O d0
by (le_lt_trans . . . previous H5)
we proved lt O n
by (lt_plus_minus . . previous)
eq nat n (S (plus O (minus n (S O))))
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
lt d0 n
→(ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2)
end of h3
by (lt_eq_gt_e . . . h1 h2 h3)
we proved
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
∀e:C
.∀u0:T
.∀d0:nat
.∀H3:getl d0 c0 (CHead e (Bind Void) u0)
.∀a:C
.∀H4:drop (S O) d0 c0 a
.ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
case ty3_abst : n:nat c0:C d:C u:T H0:getl n c0 (CHead d (Bind Abst) u) t:T H1:ty3 g d u t ⇒
the thesis becomes
∀e:C
.∀u0:T
.∀d0:nat
.∀H3:getl d0 c0 (CHead e (Bind Void) u0)
.∀a:C
.∀H4:drop (S O) d0 c0 a
.ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O u) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
(H2) by induction hypothesis we know
∀e:C
.∀u0:T
.∀d0:nat
.getl d0 d (CHead e (Bind Void) u0)
→∀a:C
.drop (S O) d0 d a
→ex3_2 T T λy1:T.λ:T.eq T u (lift (S O) d0 y1) λ:T.λy2:T.eq T t (lift (S O) d0 y2) λy1:T.λy2:T.ty3 g a y1 y2
assume e: C
assume u0: T
assume d0: nat
suppose H3: getl d0 c0 (CHead e (Bind Void) u0)
assume a: C
suppose H4: drop (S O) d0 c0 a
(h1)
suppose H5: lt n d0
(H6)
by (minus_x_Sy . . H5)
we proved eq nat (minus d0 n) (S (minus d0 (S n)))
we proceed by induction on the previous result to prove
getl
S (minus d0 (S n))
CHead d (Bind Abst) u
CHead e (Bind Void) u0
case refl_equal : ⇒
the thesis becomes
getl
minus d0 n
CHead d (Bind Abst) u
CHead e (Bind Void) u0
consider H5
we proved lt n d0
that is equivalent to le (S n) d0
by (le_S . . previous)
we proved le (S n) (S d0)
by (le_S_n . . previous)
we proved le n d0
by (getl_conf_le . . . H3 . . H0 previous)
getl
minus d0 n
CHead d (Bind Abst) u
CHead e (Bind Void) u0
getl
S (minus d0 (S n))
CHead d (Bind Abst) u
CHead e (Bind Void) u0
end of H6
(H7)
by (lt_plus_minus . . H5)
we proved eq nat d0 (S (plus n (minus d0 (S n))))
we proceed by induction on the previous result to prove drop (S O) (S (plus n (minus d0 (S n)))) c0 a
case refl_equal : ⇒
the thesis becomes the hypothesis H4
drop (S O) (S (plus n (minus d0 (S n)))) c0 a
end of H7
by (getl_drop_conf_lt . . . . . H0 . . . H7)
we proved
ex3_2
T
C
λv:T.λ:C.eq T u (lift (S O) (minus d0 (S n)) v)
λv:T.λe0:C.getl n a (CHead e0 (Bind Abst) v)
λ:T.λe0:C.drop (S O) (minus d0 (S n)) d e0
we proceed by induction on the previous result to prove
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O u) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
case ex3_2_intro : x0:T x1:C H8:eq T u (lift (S O) (minus d0 (S n)) x0) H9:getl n a (CHead x1 (Bind Abst) x0) H10:drop (S O) (minus d0 (S n)) d x1 ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O u) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
(H11)
we proceed by induction on H8 to prove
∀e0:C
.∀u1:T
.∀d1:nat
.getl d1 d (CHead e0 (Bind Void) u1)
→∀a0:C
.drop (S O) d1 d a0
→(ex3_2
T
T
λy1:T.λ:T.eq T (lift (S O) (minus d0 (S n)) x0) (lift (S O) d1 y1)
λ:T.λy2:T.eq T t (lift (S O) d1 y2)
λy1:T.λy2:T.ty3 g a0 y1 y2)
case refl_equal : ⇒
the thesis becomes the hypothesis H2
∀e0:C
.∀u1:T
.∀d1:nat
.getl d1 d (CHead e0 (Bind Void) u1)
→∀a0:C
.drop (S O) d1 d a0
→(ex3_2
T
T
λy1:T.λ:T.eq T (lift (S O) (minus d0 (S n)) x0) (lift (S O) d1 y1)
λ:T.λy2:T.eq T t (lift (S O) d1 y2)
λy1:T.λy2:T.ty3 g a0 y1 y2)
end of H11
(H12)
we proceed by induction on H8 to prove ty3 g d (lift (S O) (minus d0 (S n)) x0) t
case refl_equal : ⇒
the thesis becomes the hypothesis H1
ty3 g d (lift (S O) (minus d0 (S n)) x0) t
end of H12
(H13)
by (getl_gen_S . . . . . H6)
we proved
getl
r (Bind Abst) (minus d0 (S n))
d
CHead e (Bind Void) u0
that is equivalent to getl (minus d0 (S n)) d (CHead e (Bind Void) u0)
by (H11 . . . previous . H10)
ex3_2
T
T
λy1:T
.λ:T
.eq
T
lift (S O) (minus d0 (S n)) x0
lift (S O) (minus d0 (S n)) y1
λ:T.λy2:T.eq T t (lift (S O) (minus d0 (S n)) y2)
λy1:T.λy2:T.ty3 g x1 y1 y2
end of H13
we proceed by induction on H13 to prove
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T
.λy2:T
.eq
T
lift (S n) O (lift (S O) (minus d0 (S n)) x0)
lift (S O) d0 y2
λy1:T.λy2:T.ty3 g a y1 y2
case ex3_2_intro : x2:T x3:T H14:eq T (lift (S O) (minus d0 (S n)) x0) (lift (S O) (minus d0 (S n)) x2) H15:eq T t (lift (S O) (minus d0 (S n)) x3) H16:ty3 g x1 x2 x3 ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T
.λy2:T
.eq
T
lift (S n) O (lift (S O) (minus d0 (S n)) x0)
lift (S O) d0 y2
λy1:T.λy2:T.ty3 g a y1 y2
(H18)
by (lift_inj . . . . H14)
we proved eq T x0 x2
by (eq_ind_r . . . H16 . previous)
ty3 g x1 x0 x3
end of H18
by (le_O_n .)
we proved le O (minus d0 (S n))
by (lift_d . . . . . previous)
we proved
eq
T
lift (S O) (plus (S n) (minus d0 (S n))) (lift (S n) O x0)
lift (S n) O (lift (S O) (minus d0 (S n)) x0)
we proceed by induction on the previous result to prove
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T
.λy2:T
.eq
T
lift (S n) O (lift (S O) (minus d0 (S n)) x0)
lift (S O) d0 y2
λy1:T.λy2:T.ty3 g a y1 y2
case refl_equal : ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T
.λy2:T
.eq
T
lift (S O) (plus (S n) (minus d0 (S n))) (lift (S n) O x0)
lift (S O) d0 y2
λy1:T.λy2:T.ty3 g a y1 y2
consider H5
we proved lt n d0
that is equivalent to le (S n) d0
by (le_plus_minus . . previous)
we proved eq nat d0 (plus (S n) (minus d0 (S n)))
we proceed by induction on the previous result to prove
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T
.λy2:T
.eq
T
lift (S O) (plus (S n) (minus d0 (S n))) (lift (S n) O x0)
lift (S O) d0 y2
λy1:T.λy2:T.ty3 g a y1 y2
case refl_equal : ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S O) d0 (lift (S n) O x0)) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
(h1)
(h1)
by (refl_equal . .)
eq T (TLRef n) (TLRef n)
end of h1
(h2)
by (lift_lref_lt . . . H5)
eq T (lift (S O) d0 (TLRef n)) (TLRef n)
end of h2
by (eq_ind_r . . . h1 . h2)
eq T (TLRef n) (lift (S O) d0 (TLRef n))
end of h1
(h2)
by (refl_equal . .)
eq
T
lift (S O) d0 (lift (S n) O x0)
lift (S O) d0 (lift (S n) O x0)
end of h2
(h3)
by (ty3_abst . . . . . H9 . H18)
ty3 g a (TLRef n) (lift (S n) O x0)
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S O) d0 (lift (S n) O x0)) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T
.λy2:T
.eq
T
lift (S O) (plus (S n) (minus d0 (S n))) (lift (S n) O x0)
lift (S O) d0 y2
λy1:T.λy2:T.ty3 g a y1 y2
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T
.λy2:T
.eq
T
lift (S n) O (lift (S O) (minus d0 (S n)) x0)
lift (S O) d0 y2
λy1:T.λy2:T.ty3 g a y1 y2
we proved
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T
.λy2:T
.eq
T
lift (S n) O (lift (S O) (minus d0 (S n)) x0)
lift (S O) d0 y2
λy1:T.λy2:T.ty3 g a y1 y2
by (eq_ind_r . . . previous . H8)
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O u) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
we proved
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O u) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
lt n d0
→(ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O u) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2)
end of h1
(h2)
suppose H5: eq nat n d0
(H7)
by (eq_ind_r . . . H3 . H5)
getl n c0 (CHead e (Bind Void) u0)
end of H7
we proceed by induction on H5 to prove
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O u) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
case refl_equal : ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) n y1)
λ:T.λy2:T.eq T (lift (S n) O u) (lift (S O) n y2)
λy1:T.λy2:T.ty3 g a y1 y2
(H9)
by (getl_mono . . . H0 . H7)
we proved eq C (CHead d (Bind Abst) u) (CHead e (Bind Void) u0)
we proceed by induction on the previous result to prove
<λ:C.Prop>
CASE CHead e (Bind Void) u0 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:C.Prop>
CASE CHead d (Bind Abst) u OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
consider I
we proved True
<λ:C.Prop>
CASE CHead d (Bind Abst) u OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
<λ:C.Prop>
CASE CHead e (Bind Void) u0 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
end of H9
consider H9
we proved
<λ:C.Prop>
CASE CHead e (Bind Void) u0 OF
CSort ⇒False
| CHead k ⇒
<λ:K.Prop>
CASE k OF
Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
| Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) n y1)
λ:T.λy2:T.eq T (lift (S n) O u) (lift (S O) n y2)
λy1:T.λy2:T.ty3 g a y1 y2
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) n y1)
λ:T.λy2:T.eq T (lift (S n) O u) (lift (S O) n y2)
λy1:T.λy2:T.ty3 g a y1 y2
we proved
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O u) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
eq nat n d0
→(ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O u) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2)
end of h2
(h3)
suppose H5: lt d0 n
(h1)
by (refl_equal . .)
we proved
eq
nat
S (plus O (minus n (S O)))
S (plus O (minus n (S O)))
that is equivalent to
eq
nat
plus (S O) (minus n (S O))
S (plus O (minus n (S O)))
we proceed by induction on the previous result to prove
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef (S (plus O (minus n (S O))))) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O u) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
case refl_equal : ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef (plus (S O) (minus n (S O)))) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O u) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
(h1)
(h1)
(h1)
by (refl_equal . .)
eq
T
TLRef (plus (minus n (S O)) (S O))
TLRef (plus (minus n (S O)) (S O))
end of h1
(h2)
by (lt_le_minus . . H5)
we proved le d0 (minus n (S O))
by (lift_lref_ge . . . previous)
eq
T
lift (S O) d0 (TLRef (minus n (S O)))
TLRef (plus (minus n (S O)) (S O))
end of h2
by (eq_ind_r . . . h1 . h2)
eq
T
TLRef (plus (minus n (S O)) (S O))
lift (S O) d0 (TLRef (minus n (S O)))
end of h1
(h2)
(h1)
by (refl_equal . .)
we proved eq T (lift (S n) O u) (lift (S n) O u)
eq T (lift (S n) O u) (lift (plus (S O) n) O u)
end of h1
(h2)
(h1)
consider H5
we proved lt d0 n
that is equivalent to le (S d0) (plus O n)
by (le_S . . previous)
we proved le (S d0) (S (plus O n))
by (le_S_n . . previous)
le d0 (plus O n)
end of h1
(h2) by (le_O_n .) we proved le O d0
by (lift_free . . . . . h1 h2)
eq T (lift (S O) d0 (lift n O u)) (lift (plus (S O) n) O u)
end of h2
by (eq_ind_r . . . h1 . h2)
eq T (lift (S n) O u) (lift (S O) d0 (lift n O u))
end of h2
(h3)
(h1)
(h1)
consider H5
we proved lt d0 n
le (plus (S O) d0) n
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)) n
by (getl_drop_conf_ge . . . H0 . . . H4 previous)
we proved getl (minus n (S O)) a (CHead d (Bind Abst) u)
by (ty3_abst . . . . . previous . H1)
ty3 g a (TLRef (minus n (S O))) (lift (S (minus n (S O))) O u)
end of h1
(h2)
by (le_O_n .)
we proved le O d0
by (le_lt_trans . . . previous H5)
we proved lt O n
by (minus_x_SO . previous)
eq nat n (S (minus n (S O)))
end of h2
by (eq_ind_r . . . h1 . h2)
ty3 g a (TLRef (minus n (S O))) (lift n O u)
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef (plus (minus n (S O)) (S O))) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O u) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
end of h1
(h2)
by (plus_sym . .)
eq
nat
plus (S O) (minus n (S O))
plus (minus n (S O)) (S O)
end of h2
by (eq_ind_r . . . h1 . h2)
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef (plus (S O) (minus n (S O)))) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O u) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef (S (plus O (minus n (S O))))) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O u) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
end of h1
(h2)
by (le_O_n .)
we proved le O d0
by (le_lt_trans . . . previous H5)
we proved lt O n
by (lt_plus_minus . . previous)
eq nat n (S (plus O (minus n (S O))))
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O u) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
lt d0 n
→(ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O u) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2)
end of h3
by (lt_eq_gt_e . . . h1 h2 h3)
we proved
ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O u) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
∀e:C
.∀u0:T
.∀d0:nat
.∀H3:getl d0 c0 (CHead e (Bind Void) u0)
.∀a:C
.∀H4:drop (S O) d0 c0 a
.ex3_2
T
T
λy1:T.λ:T.eq T (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S n) O u) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
case ty3_bind : c0:C u:T t:T H0:ty3 g c0 u t b:B t3:T t4:T H2:ty3 g (CHead c0 (Bind b) u) t3 t4 ⇒
the thesis becomes
∀e:C
.∀u0:T
.∀d:nat
.∀H4:getl d c0 (CHead e (Bind Void) u0)
.∀a:C
.∀H5:drop (S O) d c0 a
.ex3_2
T
T
λy1:T.λ:T.eq T (THead (Bind b) u t3) (lift (S O) d y1)
λ:T.λy2:T.eq T (THead (Bind b) u t4) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
(H1) by induction hypothesis we know
∀e:C
.∀u0:T
.∀d:nat
.getl d c0 (CHead e (Bind Void) u0)
→∀a:C
.drop (S O) d c0 a
→(ex3_2
T
T
λy1:T.λ:T.eq T u (lift (S O) d y1)
λ:T.λy2:T.eq T t (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2)
(H3) by induction hypothesis we know
∀e:C
.∀u0:T
.∀d:nat
.getl d (CHead c0 (Bind b) u) (CHead e (Bind Void) u0)
→∀a:C
.drop (S O) d (CHead c0 (Bind b) u) a
→ex3_2 T T λy1:T.λ:T.eq T t3 (lift (S O) d y1) λ:T.λy2:T.eq T t4 (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
assume e: C
assume u0: T
assume d: nat
suppose H4: getl d c0 (CHead e (Bind Void) u0)
assume a: C
suppose H5: drop (S O) d c0 a
(H6)
by (H1 . . . H4 . H5)
ex3_2
T
T
λy1:T.λ:T.eq T u (lift (S O) d y1)
λ:T.λy2:T.eq T t (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
end of H6
we proceed by induction on H6 to prove
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Bind b) u t3) (lift (S O) d y1)
λ:T.λy2:T.eq T (THead (Bind b) u t4) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
case ex3_2_intro : x0:T x1:T H7:eq T u (lift (S O) d x0) H8:eq T t (lift (S O) d x1) H9:ty3 g a x0 x1 ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Bind b) u t3) (lift (S O) d y1)
λ:T.λy2:T.eq T (THead (Bind b) u t4) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
(H10)
we proceed by induction on H8 to prove ty3 g c0 u (lift (S O) d x1)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
ty3 g c0 u (lift (S O) d x1)
end of H10
(H12)
we proceed by induction on H7 to prove
∀e0:C
.∀u1:T
.∀d0:nat
.getl d0 (CHead c0 (Bind b) (lift (S O) d x0)) (CHead e0 (Bind Void) u1)
→∀a0:C
.drop (S O) d0 (CHead c0 (Bind b) (lift (S O) d x0)) a0
→ex3_2 T T λy1:T.λ:T.eq T t3 (lift (S O) d0 y1) λ:T.λy2:T.eq T t4 (lift (S O) d0 y2) λy1:T.λy2:T.ty3 g a0 y1 y2
case refl_equal : ⇒
the thesis becomes the hypothesis H3
∀e0:C
.∀u1:T
.∀d0:nat
.getl d0 (CHead c0 (Bind b) (lift (S O) d x0)) (CHead e0 (Bind Void) u1)
→∀a0:C
.drop (S O) d0 (CHead c0 (Bind b) (lift (S O) d x0)) a0
→ex3_2 T T λy1:T.λ:T.eq T t3 (lift (S O) d0 y1) λ:T.λy2:T.eq T t4 (lift (S O) d0 y2) λy1:T.λy2:T.ty3 g a0 y1 y2
end of H12
(H14)
(h1)
consider H4
we proved getl d c0 (CHead e (Bind Void) u0)
that is equivalent to getl (r (Bind b) d) c0 (CHead e (Bind Void) u0)
by (getl_head . . . . previous .)
getl
S d
CHead c0 (Bind b) (lift (S O) d x0)
CHead e (Bind Void) u0
end of h1
(h2)
by (drop_skip_bind . . . . H5 . .)
drop
S O
S d
CHead c0 (Bind b) (lift (S O) d x0)
CHead a (Bind b) x0
end of h2
by (H12 . . . h1 . h2)
ex3_2
T
T
λy1:T.λ:T.eq T t3 (lift (S O) (S d) y1)
λ:T.λy2:T.eq T t4 (lift (S O) (S d) y2)
λy1:T.λy2:T.ty3 g (CHead a (Bind b) x0) y1 y2
end of H14
we proceed by induction on H14 to prove
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Bind b) (lift (S O) d x0) t3) (lift (S O) d y1)
λ:T.λy2:T.eq T (THead (Bind b) (lift (S O) d x0) t4) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
case ex3_2_intro : x2:T x3:T H15:eq T t3 (lift (S O) (S d) x2) H16:eq T t4 (lift (S O) (S d) x3) H17:ty3 g (CHead a (Bind b) x0) x2 x3 ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Bind b) (lift (S O) d x0) t3) (lift (S O) d y1)
λ:T.λy2:T.eq T (THead (Bind b) (lift (S O) d x0) t4) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
(h1)
by (lift_bind . . . . .)
we proved
eq
T
lift (S O) d (THead (Bind b) x0 x2)
THead (Bind b) (lift (S O) d x0) (lift (S O) (S d) x2)
by (sym_eq . . . previous)
eq
T
THead (Bind b) (lift (S O) d x0) (lift (S O) (S d) x2)
lift (S O) d (THead (Bind b) x0 x2)
end of h1
(h2)
by (lift_bind . . . . .)
we proved
eq
T
lift (S O) d (THead (Bind b) x0 x3)
THead (Bind b) (lift (S O) d x0) (lift (S O) (S d) x3)
by (sym_eq . . . previous)
eq
T
THead (Bind b) (lift (S O) d x0) (lift (S O) (S d) x3)
lift (S O) d (THead (Bind b) x0 x3)
end of h2
(h3)
by (ty3_bind . . . . H9 . . . H17)
ty3 g a (THead (Bind b) x0 x2) (THead (Bind b) x0 x3)
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
we proved
ex3_2
T
T
λy1:T
.λ:T
.eq
T
THead (Bind b) (lift (S O) d x0) (lift (S O) (S d) x2)
lift (S O) d y1
λ:T
.λy2:T
.eq
T
THead (Bind b) (lift (S O) d x0) (lift (S O) (S d) x3)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
by (eq_ind_r . . . previous . H15)
we proved
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Bind b) (lift (S O) d x0) t3) (lift (S O) d y1)
λ:T
.λy2:T
.eq
T
THead (Bind b) (lift (S O) d x0) (lift (S O) (S d) x3)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
by (eq_ind_r . . . previous . H16)
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Bind b) (lift (S O) d x0) t3) (lift (S O) d y1)
λ:T.λy2:T.eq T (THead (Bind b) (lift (S O) d x0) t4) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
we proved
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Bind b) (lift (S O) d x0) t3) (lift (S O) d y1)
λ:T.λy2:T.eq T (THead (Bind b) (lift (S O) d x0) t4) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
by (eq_ind_r . . . previous . H7)
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Bind b) u t3) (lift (S O) d y1)
λ:T.λy2:T.eq T (THead (Bind b) u t4) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
we proved
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Bind b) u t3) (lift (S O) d y1)
λ:T.λy2:T.eq T (THead (Bind b) u t4) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
∀e:C
.∀u0:T
.∀d:nat
.∀H4:getl d c0 (CHead e (Bind Void) u0)
.∀a:C
.∀H5:drop (S O) d c0 a
.ex3_2
T
T
λy1:T.λ:T.eq T (THead (Bind b) u t3) (lift (S O) d y1)
λ:T.λy2:T.eq T (THead (Bind b) u t4) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
case ty3_appl : c0:C w:T u:T :ty3 g c0 w u v:T t:T H2:ty3 g c0 v (THead (Bind Abst) u t) ⇒
the thesis becomes
∀e:C
.∀u0:T
.∀d:nat
.∀H4:getl d c0 (CHead e (Bind Void) u0)
.∀a:C
.∀H5:drop (S O) d c0 a
.ex3_2
T
T
λy1:T.λ:T.eq T (THead (Flat Appl) w v) (lift (S O) d y1)
λ:T
.λy2:T
.eq
T
THead (Flat Appl) w (THead (Bind Abst) u t)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
(H1) by induction hypothesis we know
∀e:C
.∀u0:T
.∀d:nat
.getl d c0 (CHead e (Bind Void) u0)
→∀a:C
.drop (S O) d c0 a
→(ex3_2
T
T
λy1:T.λ:T.eq T w (lift (S O) d y1)
λ:T.λy2:T.eq T u (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2)
(H3) by induction hypothesis we know
∀e:C
.∀u0:T
.∀d:nat
.getl d c0 (CHead e (Bind Void) u0)
→∀a:C
.drop (S O) d c0 a
→(ex3_2
T
T
λy1:T.λ:T.eq T v (lift (S O) d y1)
λ:T.λy2:T.eq T (THead (Bind Abst) u t) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2)
assume e: C
assume u0: T
assume d: nat
suppose H4: getl d c0 (CHead e (Bind Void) u0)
assume a: C
suppose H5: drop (S O) d c0 a
(H6)
by (H3 . . . H4 . H5)
ex3_2
T
T
λy1:T.λ:T.eq T v (lift (S O) d y1)
λ:T.λy2:T.eq T (THead (Bind Abst) u t) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
end of H6
we proceed by induction on H6 to prove
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Flat Appl) w v) (lift (S O) d y1)
λ:T
.λy2:T
.eq
T
THead (Flat Appl) w (THead (Bind Abst) u t)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
case ex3_2_intro : x0:T x1:T H7:eq T v (lift (S O) d x0) H8:eq T (THead (Bind Abst) u t) (lift (S O) d x1) H9:ty3 g a x0 x1 ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Flat Appl) w v) (lift (S O) d y1)
λ:T
.λy2:T
.eq
T
THead (Flat Appl) w (THead (Bind Abst) u t)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
by (lift_gen_bind . . . . . . H8)
we proved
ex3_2
T
T
λy:T.λz:T.eq T x1 (THead (Bind Abst) y z)
λy:T.λ:T.eq T u (lift (S O) d y)
λ:T.λz:T.eq T t (lift (S O) (S d) z)
we proceed by induction on the previous result to prove
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Flat Appl) w (lift (S O) d x0)) (lift (S O) d y1)
λ:T
.λy2:T
.eq
T
THead (Flat Appl) w (THead (Bind Abst) u t)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
case ex3_2_intro : x2:T x3:T H11:eq T x1 (THead (Bind Abst) x2 x3) H12:eq T u (lift (S O) d x2) H13:eq T t (lift (S O) (S d) x3) ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Flat Appl) w (lift (S O) d x0)) (lift (S O) d y1)
λ:T
.λy2:T
.eq
T
THead (Flat Appl) w (THead (Bind Abst) u t)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
(H14)
we proceed by induction on H11 to prove ty3 g a x0 (THead (Bind Abst) x2 x3)
case refl_equal : ⇒
the thesis becomes the hypothesis H9
ty3 g a x0 (THead (Bind Abst) x2 x3)
end of H14
(H15)
we proceed by induction on H12 to prove
∀e0:C
.∀u1:T
.∀d0:nat
.getl d0 c0 (CHead e0 (Bind Void) u1)
→∀a0:C
.drop (S O) d0 c0 a0
→(ex3_2
T
T
λy1:T.λ:T.eq T w (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S O) d x2) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a0 y1 y2)
case refl_equal : ⇒
the thesis becomes the hypothesis H1
∀e0:C
.∀u1:T
.∀d0:nat
.getl d0 c0 (CHead e0 (Bind Void) u1)
→∀a0:C
.drop (S O) d0 c0 a0
→(ex3_2
T
T
λy1:T.λ:T.eq T w (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S O) d x2) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a0 y1 y2)
end of H15
(H16)
by (H15 . . . H4 . H5)
ex3_2
T
T
λy1:T.λ:T.eq T w (lift (S O) d y1)
λ:T.λy2:T.eq T (lift (S O) d x2) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
end of H16
we proceed by induction on H16 to prove
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Flat Appl) w (lift (S O) d x0)) (lift (S O) d y1)
λ:T
.λy2:T
.eq
T
THead
Flat Appl
w
THead (Bind Abst) (lift (S O) d x2) (lift (S O) (S d) x3)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
case ex3_2_intro : x4:T x5:T H17:eq T w (lift (S O) d x4) H18:eq T (lift (S O) d x2) (lift (S O) d x5) H19:ty3 g a x4 x5 ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Flat Appl) w (lift (S O) d x0)) (lift (S O) d y1)
λ:T
.λy2:T
.eq
T
THead
Flat Appl
w
THead (Bind Abst) (lift (S O) d x2) (lift (S O) (S d) x3)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
(H20)
by (lift_inj . . . . H18)
we proved eq T x2 x5
by (eq_ind_r . . . H19 . previous)
ty3 g a x4 x2
end of H20
by (lift_bind . . . . .)
we proved
eq
T
lift (S O) d (THead (Bind Abst) x2 x3)
THead (Bind Abst) (lift (S O) d x2) (lift (S O) (S d) x3)
we proceed by induction on the previous result to prove
ex3_2
T
T
λy1:T
.λ:T
.eq
T
THead (Flat Appl) (lift (S O) d x4) (lift (S O) d x0)
lift (S O) d y1
λ:T
.λy2:T
.eq
T
THead
Flat Appl
lift (S O) d x4
THead (Bind Abst) (lift (S O) d x2) (lift (S O) (S d) x3)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
case refl_equal : ⇒
the thesis becomes
ex3_2
T
T
λy1:T
.λ:T
.eq
T
THead (Flat Appl) (lift (S O) d x4) (lift (S O) d x0)
lift (S O) d y1
λ:T
.λy2:T
.eq
T
THead
Flat Appl
lift (S O) d x4
lift (S O) d (THead (Bind Abst) x2 x3)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
by (lift_flat . . . . .)
we proved
eq
T
lift (S O) d (THead (Flat Appl) x4 x0)
THead (Flat Appl) (lift (S O) d x4) (lift (S O) d x0)
we proceed by induction on the previous result to prove
ex3_2
T
T
λy1:T
.λ:T
.eq
T
THead (Flat Appl) (lift (S O) d x4) (lift (S O) d x0)
lift (S O) d y1
λ:T
.λy2:T
.eq
T
THead
Flat Appl
lift (S O) d x4
lift (S O) d (THead (Bind Abst) x2 x3)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
case refl_equal : ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.eq T (lift (S O) d (THead (Flat Appl) x4 x0)) (lift (S O) d y1)
λ:T
.λy2:T
.eq
T
THead
Flat Appl
lift (S O) d x4
lift (S O) d (THead (Bind Abst) x2 x3)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
by (lift_flat . . . . .)
we proved
eq
T
lift (S O) d (THead (Flat Appl) x4 (THead (Bind Abst) x2 x3))
THead
Flat Appl
lift (S O) d x4
lift (S O) d (THead (Bind Abst) x2 x3)
we proceed by induction on the previous result to prove
ex3_2
T
T
λy1:T.λ:T.eq T (lift (S O) d (THead (Flat Appl) x4 x0)) (lift (S O) d y1)
λ:T
.λy2:T
.eq
T
THead
Flat Appl
lift (S O) d x4
lift (S O) d (THead (Bind Abst) x2 x3)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
case refl_equal : ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.eq T (lift (S O) d (THead (Flat Appl) x4 x0)) (lift (S O) d y1)
λ:T
.λy2:T
.eq
T
lift (S O) d (THead (Flat Appl) x4 (THead (Bind Abst) x2 x3))
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
(h1)
by (refl_equal . .)
eq
T
lift (S O) d (THead (Flat Appl) x4 x0)
lift (S O) d (THead (Flat Appl) x4 x0)
end of h1
(h2)
by (refl_equal . .)
eq
T
lift (S O) d (THead (Flat Appl) x4 (THead (Bind Abst) x2 x3))
lift (S O) d (THead (Flat Appl) x4 (THead (Bind Abst) x2 x3))
end of h2
(h3)
by (ty3_appl . . . . H20 . . H14)
ty3
g
a
THead (Flat Appl) x4 x0
THead (Flat Appl) x4 (THead (Bind Abst) x2 x3)
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
ex3_2
T
T
λy1:T.λ:T.eq T (lift (S O) d (THead (Flat Appl) x4 x0)) (lift (S O) d y1)
λ:T
.λy2:T
.eq
T
lift (S O) d (THead (Flat Appl) x4 (THead (Bind Abst) x2 x3))
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
ex3_2
T
T
λy1:T.λ:T.eq T (lift (S O) d (THead (Flat Appl) x4 x0)) (lift (S O) d y1)
λ:T
.λy2:T
.eq
T
THead
Flat Appl
lift (S O) d x4
lift (S O) d (THead (Bind Abst) x2 x3)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
ex3_2
T
T
λy1:T
.λ:T
.eq
T
THead (Flat Appl) (lift (S O) d x4) (lift (S O) d x0)
lift (S O) d y1
λ:T
.λy2:T
.eq
T
THead
Flat Appl
lift (S O) d x4
lift (S O) d (THead (Bind Abst) x2 x3)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
we proved
ex3_2
T
T
λy1:T
.λ:T
.eq
T
THead (Flat Appl) (lift (S O) d x4) (lift (S O) d x0)
lift (S O) d y1
λ:T
.λy2:T
.eq
T
THead
Flat Appl
lift (S O) d x4
THead (Bind Abst) (lift (S O) d x2) (lift (S O) (S d) x3)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
by (eq_ind_r . . . previous . H17)
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Flat Appl) w (lift (S O) d x0)) (lift (S O) d y1)
λ:T
.λy2:T
.eq
T
THead
Flat Appl
w
THead (Bind Abst) (lift (S O) d x2) (lift (S O) (S d) x3)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
we proved
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Flat Appl) w (lift (S O) d x0)) (lift (S O) d y1)
λ:T
.λy2:T
.eq
T
THead
Flat Appl
w
THead (Bind Abst) (lift (S O) d x2) (lift (S O) (S d) x3)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
by (eq_ind_r . . . previous . H12)
we proved
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Flat Appl) w (lift (S O) d x0)) (lift (S O) d y1)
λ:T
.λy2:T
.eq
T
THead
Flat Appl
w
THead (Bind Abst) u (lift (S O) (S d) x3)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
by (eq_ind_r . . . previous . H13)
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Flat Appl) w (lift (S O) d x0)) (lift (S O) d y1)
λ:T
.λy2:T
.eq
T
THead (Flat Appl) w (THead (Bind Abst) u t)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
we proved
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Flat Appl) w (lift (S O) d x0)) (lift (S O) d y1)
λ:T
.λy2:T
.eq
T
THead (Flat Appl) w (THead (Bind Abst) u t)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
by (eq_ind_r . . . previous . H7)
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Flat Appl) w v) (lift (S O) d y1)
λ:T
.λy2:T
.eq
T
THead (Flat Appl) w (THead (Bind Abst) u t)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
we proved
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Flat Appl) w v) (lift (S O) d y1)
λ:T
.λy2:T
.eq
T
THead (Flat Appl) w (THead (Bind Abst) u t)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
∀e:C
.∀u0:T
.∀d:nat
.∀H4:getl d c0 (CHead e (Bind Void) u0)
.∀a:C
.∀H5:drop (S O) d c0 a
.ex3_2
T
T
λy1:T.λ:T.eq T (THead (Flat Appl) w v) (lift (S O) d y1)
λ:T
.λy2:T
.eq
T
THead (Flat Appl) w (THead (Bind Abst) u t)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
case ty3_cast : c0:C t3:T t4:T H0:ty3 g c0 t3 t4 t0:T H2:ty3 g c0 t4 t0 ⇒
the thesis becomes
∀e:C
.∀u:T
.∀d:nat
.∀H4:getl d c0 (CHead e (Bind Void) u)
.∀a:C
.∀H5:drop (S O) d c0 a
.ex3_2
T
T
λy1:T.λ:T.eq T (THead (Flat Cast) t4 t3) (lift (S O) d y1)
λ:T.λy2:T.eq T (THead (Flat Cast) t0 t4) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
(H1) by induction hypothesis we know
∀e:C
.∀u:T
.∀d:nat
.getl d c0 (CHead e (Bind Void) u)
→∀a:C
.drop (S O) d c0 a
→ex3_2 T T λy1:T.λ:T.eq T t3 (lift (S O) d y1) λ:T.λy2:T.eq T t4 (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
(H3) by induction hypothesis we know
∀e:C
.∀u:T
.∀d:nat
.getl d c0 (CHead e (Bind Void) u)
→∀a:C
.drop (S O) d c0 a
→ex3_2 T T λy1:T.λ:T.eq T t4 (lift (S O) d y1) λ:T.λy2:T.eq T t0 (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
assume e: C
assume u: T
assume d: nat
suppose H4: getl d c0 (CHead e (Bind Void) u)
assume a: C
suppose H5: drop (S O) d c0 a
(H6)
by (H3 . . . H4 . H5)
ex3_2 T T λy1:T.λ:T.eq T t4 (lift (S O) d y1) λ:T.λy2:T.eq T t0 (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
end of H6
we proceed by induction on H6 to prove
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Flat Cast) t4 t3) (lift (S O) d y1)
λ:T.λy2:T.eq T (THead (Flat Cast) t0 t4) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
case ex3_2_intro : x0:T x1:T H7:eq T t4 (lift (S O) d x0) H8:eq T t0 (lift (S O) d x1) H9:ty3 g a x0 x1 ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Flat Cast) t4 t3) (lift (S O) d y1)
λ:T.λy2:T.eq T (THead (Flat Cast) t0 t4) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
(H10)
we proceed by induction on H8 to prove ty3 g c0 t4 (lift (S O) d x1)
case refl_equal : ⇒
the thesis becomes the hypothesis H2
ty3 g c0 t4 (lift (S O) d x1)
end of H10
(H12)
we proceed by induction on H7 to prove
∀e0:C
.∀u0:T
.∀d0:nat
.getl d0 c0 (CHead e0 (Bind Void) u0)
→∀a0:C
.drop (S O) d0 c0 a0
→(ex3_2
T
T
λy1:T.λ:T.eq T t3 (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S O) d x0) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a0 y1 y2)
case refl_equal : ⇒
the thesis becomes the hypothesis H1
∀e0:C
.∀u0:T
.∀d0:nat
.getl d0 c0 (CHead e0 (Bind Void) u0)
→∀a0:C
.drop (S O) d0 c0 a0
→(ex3_2
T
T
λy1:T.λ:T.eq T t3 (lift (S O) d0 y1)
λ:T.λy2:T.eq T (lift (S O) d x0) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a0 y1 y2)
end of H12
(H13)
we proceed by induction on H7 to prove ty3 g c0 t3 (lift (S O) d x0)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
ty3 g c0 t3 (lift (S O) d x0)
end of H13
(H14)
by (H12 . . . H4 . H5)
ex3_2
T
T
λy1:T.λ:T.eq T t3 (lift (S O) d y1)
λ:T.λy2:T.eq T (lift (S O) d x0) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
end of H14
we proceed by induction on H14 to prove
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Flat Cast) (lift (S O) d x0) t3) (lift (S O) d y1)
λ:T
.λy2:T
.eq
T
THead (Flat Cast) (lift (S O) d x1) (lift (S O) d x0)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
case ex3_2_intro : x2:T x3:T H15:eq T t3 (lift (S O) d x2) H16:eq T (lift (S O) d x0) (lift (S O) d x3) H17:ty3 g a x2 x3 ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Flat Cast) (lift (S O) d x0) t3) (lift (S O) d y1)
λ:T
.λy2:T
.eq
T
THead (Flat Cast) (lift (S O) d x1) (lift (S O) d x0)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
(H19)
by (lift_inj . . . . H16)
we proved eq T x0 x3
by (eq_ind_r . . . H17 . previous)
ty3 g a x2 x0
end of H19
by (lift_flat . . . . .)
we proved
eq
T
lift (S O) d (THead (Flat Cast) x0 x2)
THead (Flat Cast) (lift (S O) d x0) (lift (S O) d x2)
we proceed by induction on the previous result to prove
ex3_2
T
T
λy1:T
.λ:T
.eq
T
THead (Flat Cast) (lift (S O) d x0) (lift (S O) d x2)
lift (S O) d y1
λ:T
.λy2:T
.eq
T
THead (Flat Cast) (lift (S O) d x1) (lift (S O) d x0)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
case refl_equal : ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.eq T (lift (S O) d (THead (Flat Cast) x0 x2)) (lift (S O) d y1)
λ:T
.λy2:T
.eq
T
THead (Flat Cast) (lift (S O) d x1) (lift (S O) d x0)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
by (lift_flat . . . . .)
we proved
eq
T
lift (S O) d (THead (Flat Cast) x1 x0)
THead (Flat Cast) (lift (S O) d x1) (lift (S O) d x0)
we proceed by induction on the previous result to prove
ex3_2
T
T
λy1:T.λ:T.eq T (lift (S O) d (THead (Flat Cast) x0 x2)) (lift (S O) d y1)
λ:T
.λy2:T
.eq
T
THead (Flat Cast) (lift (S O) d x1) (lift (S O) d x0)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
case refl_equal : ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.eq T (lift (S O) d (THead (Flat Cast) x0 x2)) (lift (S O) d y1)
λ:T.λy2:T.eq T (lift (S O) d (THead (Flat Cast) x1 x0)) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
(h1)
by (refl_equal . .)
eq
T
lift (S O) d (THead (Flat Cast) x0 x2)
lift (S O) d (THead (Flat Cast) x0 x2)
end of h1
(h2)
by (refl_equal . .)
eq
T
lift (S O) d (THead (Flat Cast) x1 x0)
lift (S O) d (THead (Flat Cast) x1 x0)
end of h2
(h3)
by (ty3_cast . . . . H19 . H9)
ty3 g a (THead (Flat Cast) x0 x2) (THead (Flat Cast) x1 x0)
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
ex3_2
T
T
λy1:T.λ:T.eq T (lift (S O) d (THead (Flat Cast) x0 x2)) (lift (S O) d y1)
λ:T.λy2:T.eq T (lift (S O) d (THead (Flat Cast) x1 x0)) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
ex3_2
T
T
λy1:T.λ:T.eq T (lift (S O) d (THead (Flat Cast) x0 x2)) (lift (S O) d y1)
λ:T
.λy2:T
.eq
T
THead (Flat Cast) (lift (S O) d x1) (lift (S O) d x0)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
we proved
ex3_2
T
T
λy1:T
.λ:T
.eq
T
THead (Flat Cast) (lift (S O) d x0) (lift (S O) d x2)
lift (S O) d y1
λ:T
.λy2:T
.eq
T
THead (Flat Cast) (lift (S O) d x1) (lift (S O) d x0)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
by (eq_ind_r . . . previous . H15)
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Flat Cast) (lift (S O) d x0) t3) (lift (S O) d y1)
λ:T
.λy2:T
.eq
T
THead (Flat Cast) (lift (S O) d x1) (lift (S O) d x0)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
we proved
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Flat Cast) (lift (S O) d x0) t3) (lift (S O) d y1)
λ:T
.λy2:T
.eq
T
THead (Flat Cast) (lift (S O) d x1) (lift (S O) d x0)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
by (eq_ind_r . . . previous . H7)
we proved
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Flat Cast) t4 t3) (lift (S O) d y1)
λ:T.λy2:T.eq T (THead (Flat Cast) (lift (S O) d x1) t4) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
by (eq_ind_r . . . previous . H8)
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Flat Cast) t4 t3) (lift (S O) d y1)
λ:T.λy2:T.eq T (THead (Flat Cast) t0 t4) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
we proved
ex3_2
T
T
λy1:T.λ:T.eq T (THead (Flat Cast) t4 t3) (lift (S O) d y1)
λ:T.λy2:T.eq T (THead (Flat Cast) t0 t4) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
∀e:C
.∀u:T
.∀d:nat
.∀H4:getl d c0 (CHead e (Bind Void) u)
.∀a:C
.∀H5:drop (S O) d c0 a
.ex3_2
T
T
λy1:T.λ:T.eq T (THead (Flat Cast) t4 t3) (lift (S O) d y1)
λ:T.λy2:T.eq T (THead (Flat Cast) t0 t4) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
we proved
∀e:C
.∀u:T
.∀d:nat
.getl d c (CHead e (Bind Void) u)
→∀a:C
.drop (S O) d c a
→ex3_2 T T λy1:T.λ:T.eq T t1 (lift (S O) d y1) λ:T.λy2:T.eq T t2 (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
we proved
∀g:G
.∀c:C
.∀t1:T
.∀t2:T
.ty3 g c t1 t2
→∀e:C
.∀u:T
.∀d:nat
.getl d c (CHead e (Bind Void) u)
→∀a:C
.drop (S O) d c a
→ex3_2 T T λy1:T.λ:T.eq T t1 (lift (S O) d y1) λ:T.λy2:T.eq T t2 (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2