DEFINITION ty3_gen_cabbr()
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 Abbr) u)
→∀a0:C
.csubst1 d u c a0
→∀a:C
.drop (S O) d a0 a
→ex3_2 T T λy1:T.λ:T.subst1 d u t1 (lift (S O) d y1) λ:T.λy2:T.subst1 d u 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 Abbr) u)
→∀a0:C
.csubst1 d u c a0
→∀a:C
.drop (S O) d a0 a
→ex3_2 T T λy1:T.λ:T.subst1 d u t1 (lift (S O) d y1) λ:T.λy2:T.subst1 d u t2 (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
case ty3_conv : c0:C t3:T t:T :ty3 g c0 t3 t u:T t4:T :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 Abbr) u0)
.∀a0:C
.∀H6:csubst1 d u0 c0 a0
.∀a:C
.∀H7:drop (S O) d a0 a
.ex3_2 T T λy1:T.λ:T.subst1 d u0 u (lift (S O) d y1) λ:T.λy2:T.subst1 d u0 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 Abbr) u)
→∀a0:C
.csubst1 d u c0 a0
→∀a:C
.drop (S O) d a0 a
→ex3_2 T T λy1:T.λ:T.subst1 d u t3 (lift (S O) d y1) λ:T.λy2:T.subst1 d u 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 Abbr) u0)
→∀a0:C
.csubst1 d u0 c0 a0
→∀a:C
.drop (S O) d a0 a
→ex3_2 T T λy1:T.λ:T.subst1 d u0 u (lift (S O) d y1) λ:T.λy2:T.subst1 d u0 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 Abbr) u0)
assume a0: C
suppose H6: csubst1 d u0 c0 a0
assume a: C
suppose H7: drop (S O) d a0 a
(H8)
by (H3 . . . H5 . H6 . H7)
ex3_2 T T λy1:T.λ:T.subst1 d u0 u (lift (S O) d y1) λ:T.λy2:T.subst1 d u0 t4 (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
end of H8
we proceed by induction on H8 to prove ex3_2 T T λy1:T.λ:T.subst1 d u0 u (lift (S O) d y1) λ:T.λy2:T.subst1 d u0 t3 (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
case ex3_2_intro : x0:T x1:T H9:subst1 d u0 u (lift (S O) d x0) H10:subst1 d u0 t4 (lift (S O) d x1) H11:ty3 g a x0 x1 ⇒
the thesis becomes ex3_2 T T λy1:T.λ:T.subst1 d u0 u (lift (S O) d y1) λ:T.λy2:T.subst1 d u0 t3 (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
(H12)
by (H1 . . . H5 . H6 . H7)
ex3_2 T T λy1:T.λ:T.subst1 d u0 t3 (lift (S O) d y1) λ:T.λy2:T.subst1 d u0 t (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
end of H12
we proceed by induction on H12 to prove ex3_2 T T λy1:T.λ:T.subst1 d u0 u (lift (S O) d y1) λ:T.λy2:T.subst1 d u0 t3 (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
case ex3_2_intro : x2:T x3:T H13:subst1 d u0 t3 (lift (S O) d x2) :subst1 d u0 t (lift (S O) d x3) H15:ty3 g a x2 x3 ⇒
the thesis becomes ex3_2 T T λy1:T.λ:T.subst1 d u0 u (lift (S O) d y1) λ:T.λy2:T.subst1 d u0 t3 (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
by (pc3_gen_cabbr . . . H4 . . . H5 . H6 . H7 . H10 . H13)
we proved pc3 a x1 x2
by (ty3_conv . . . . H15 . . H11 previous)
we proved ty3 g a x0 x2
by (ex3_2_intro . . . . . . . H9 H13 previous)
ex3_2 T T λy1:T.λ:T.subst1 d u0 u (lift (S O) d y1) λ:T.λy2:T.subst1 d u0 t3 (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
ex3_2 T T λy1:T.λ:T.subst1 d u0 u (lift (S O) d y1) λ:T.λy2:T.subst1 d u0 t3 (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
we proved ex3_2 T T λy1:T.λ:T.subst1 d u0 u (lift (S O) d y1) λ:T.λy2:T.subst1 d u0 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 Abbr) u0)
.∀a0:C
.∀H6:csubst1 d u0 c0 a0
.∀a:C
.∀H7:drop (S O) d a0 a
.ex3_2 T T λy1:T.λ:T.subst1 d u0 u (lift (S O) d y1) λ:T.λy2:T.subst1 d u0 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 Abbr) u)
→∀a0:C
.csubst1 d u c0 a0
→∀a:C
.drop (S O) d a0 a
→(ex3_2
T
T
λy1:T.λ:T.subst1 d u (TSort m) (lift (S O) d y1)
λ:T.λy2:T.subst1 d u (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 Abbr) u)
assume a0: C
suppose : csubst1 d u c0 a0
assume a: C
suppose : drop (S O) d a0 a
(h1)
(h1)
by (subst1_refl . . .)
subst1 d u (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)
subst1 d u (TSort m) (lift (S O) d (TSort m))
end of h1
(h2)
(h1)
by (subst1_refl . . .)
subst1 d u (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)
subst1 d u (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.subst1 d u (TSort m) (lift (S O) d y1)
λ:T.λy2:T.subst1 d u (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 Abbr) u)
→∀a0:C
.csubst1 d u c0 a0
→∀a:C
.drop (S O) d a0 a
→(ex3_2
T
T
λy1:T.λ:T.subst1 d u (TSort m) (lift (S O) d y1)
λ:T.λy2:T.subst1 d u (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 Abbr) u0)
.∀a0:C
.∀H4:csubst1 d0 u0 c0 a0
.∀a:C
.∀H5:drop (S O) d0 a0 a
.ex3_2
T
T
λy1:T.λ:T.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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 Abbr) u0)
→∀a0:C
.csubst1 d0 u0 d a0
→∀a:C
.drop (S O) d0 a0 a
→ex3_2 T T λy1:T.λ:T.subst1 d0 u0 u (lift (S O) d0 y1) λ:T.λy2:T.subst1 d0 u0 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 Abbr) u0)
assume a0: C
suppose H4: csubst1 d0 u0 c0 a0
assume a: C
suppose H5: drop (S O) d0 a0 a
(h1)
suppose H6: lt n d0
(H7)
by (minus_x_Sy . . H6)
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 Abbr) u0
case refl_equal : ⇒
the thesis becomes
getl
minus d0 n
CHead d (Bind Abbr) u
CHead e (Bind Abbr) u0
consider H6
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 Abbr) u0
getl
S (minus d0 (S n))
CHead d (Bind Abbr) u
CHead e (Bind Abbr) u0
end of H7
by (csubst1_getl_lt . . H6 . . . H4 . H0)
we proved ex2 C λe2:C.csubst1 (minus d0 n) u0 (CHead d (Bind Abbr) u) e2 λe2:C.getl n a0 e2
we proceed by induction on the previous result to prove
ex3_2
T
T
λy1:T.λ:T.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
case ex_intro2 : x:C H8:csubst1 (minus d0 n) u0 (CHead d (Bind Abbr) u) x H9:getl n a0 x ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
(H10)
by (minus_x_Sy . . H6)
we proved eq nat (minus d0 n) (S (minus d0 (S n)))
we proceed by induction on the previous result to prove csubst1 (S (minus d0 (S n))) u0 (CHead d (Bind Abbr) u) x
case refl_equal : ⇒
the thesis becomes the hypothesis H8
csubst1 (S (minus d0 (S n))) u0 (CHead d (Bind Abbr) u) x
end of H10
(H11)
consider H10
we proved csubst1 (S (minus d0 (S n))) u0 (CHead d (Bind Abbr) u) x
that is equivalent to csubst1 (s (Bind Abbr) (minus d0 (S n))) u0 (CHead d (Bind Abbr) u) x
by (csubst1_gen_head . . . . . . previous)
ex3_2
T
C
λu2:T.λc2:C.eq C x (CHead c2 (Bind Abbr) u2)
λu2:T.λ:C.subst1 (minus d0 (S n)) u0 u u2
λ:T.λc2:C.csubst1 (minus d0 (S n)) u0 d c2
end of H11
we proceed by induction on H11 to prove
ex3_2
T
T
λy1:T.λ:T.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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 H12:eq C x (CHead x1 (Bind Abbr) x0) H13:subst1 (minus d0 (S n)) u0 u x0 H14:csubst1 (minus d0 (S n)) u0 d x1 ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
(H15)
we proceed by induction on H12 to prove getl n a0 (CHead x1 (Bind Abbr) x0)
case refl_equal : ⇒
the thesis becomes the hypothesis H9
getl n a0 (CHead x1 (Bind Abbr) x0)
end of H15
(H16)
by (lt_plus_minus . . H6)
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)))) a0 a
case refl_equal : ⇒
the thesis becomes the hypothesis H5
drop (S O) (S (plus n (minus d0 (S n)))) a0 a
end of H16
by (getl_drop_conf_lt . . . . . H15 . . . H16)
we proved
ex3_2
T
C
λv:T.λ:C.eq T x0 (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)) x1 e0
we proceed by induction on the previous result to prove
ex3_2
T
T
λy1:T.λ:T.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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:C H17:eq T x0 (lift (S O) (minus d0 (S n)) x2) H18:getl n a (CHead x3 (Bind Abbr) x2) H19:drop (S O) (minus d0 (S n)) x1 x3 ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
(H20)
we proceed by induction on H17 to prove subst1 (minus d0 (S n)) u0 u (lift (S O) (minus d0 (S n)) x2)
case refl_equal : ⇒
the thesis becomes the hypothesis H13
subst1 (minus d0 (S n)) u0 u (lift (S O) (minus d0 (S n)) x2)
end of H20
(H21)
by (getl_gen_S . . . . . H7)
we proved
getl
r (Bind Abbr) (minus d0 (S n))
d
CHead e (Bind Abbr) u0
that is equivalent to getl (minus d0 (S n)) d (CHead e (Bind Abbr) u0)
by (H2 . . . previous . H14 . H19)
ex3_2
T
T
λy1:T.λ:T.subst1 (minus d0 (S n)) u0 u (lift (S O) (minus d0 (S n)) y1)
λ:T.λy2:T.subst1 (minus d0 (S n)) u0 t (lift (S O) (minus d0 (S n)) y2)
λy1:T.λy2:T.ty3 g x3 y1 y2
end of H21
we proceed by induction on H21 to prove
ex3_2
T
T
λy1:T.λ:T.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
case ex3_2_intro : x4:T x5:T H22:subst1 (minus d0 (S n)) u0 u (lift (S O) (minus d0 (S n)) x4) H23:subst1 (minus d0 (S n)) u0 t (lift (S O) (minus d0 (S n)) x5) H24:ty3 g x3 x4 x5 ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
(H25)
by (subst1_confluence_lift . . . . H22 . H20)
we proved eq T x4 x2
we proceed by induction on the previous result to prove ty3 g x3 x2 x5
case refl_equal : ⇒
the thesis becomes the hypothesis H24
ty3 g x3 x2 x5
end of H25
(h1)
(h1)
(h1)
(h1)
by (subst1_refl . . .)
subst1 d0 u0 (TLRef n) (TLRef n)
end of h1
(h2)
by (lift_lref_lt . . . H6)
eq T (lift (S O) d0 (TLRef n)) (TLRef n)
end of h2
by (eq_ind_r . . . h1 . h2)
subst1 d0 u0 (TLRef n) (lift (S O) d0 (TLRef n))
end of h1
(h2)
(h1)
by (le_O_n .)
we proved le O (minus d0 (S n))
by (subst1_lift_ge . . . . . H23 . previous)
subst1
plus (minus d0 (S n)) (S n)
u0
lift (S n) O t
lift (S n) O (lift (S O) (minus d0 (S n)) x5)
end of h1
(h2)
by (le_O_n .)
we proved le O (minus d0 (S n))
by (lift_d . . . . . previous)
eq
T
lift (S O) (plus (S n) (minus d0 (S n))) (lift (S n) O x5)
lift (S n) O (lift (S O) (minus d0 (S n)) x5)
end of h2
by (eq_ind_r . . . h1 . h2)
subst1
plus (minus d0 (S n)) (S n)
u0
lift (S n) O t
lift (S O) (plus (S n) (minus d0 (S n))) (lift (S n) O x5)
end of h2
(h3)
by (ty3_abbr . . . . . H18 . H25)
ty3 g a (TLRef n) (lift (S n) O x5)
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
ex3_2
T
T
λy1:T.λ:T.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T
.λy2:T
.subst1
plus (minus d0 (S n)) (S n)
u0
lift (S n) O t
lift (S O) (plus (S n) (minus d0 (S n))) y2
λy1:T.λy2:T.ty3 g a y1 y2
end of h1
(h2)
consider H6
we proved lt n d0
that is equivalent to le (S n) d0
by (le_plus_minus . . previous)
eq nat d0 (plus (S n) (minus d0 (S n)))
end of h2
by (eq_ind_r . . . h1 . h2)
ex3_2
T
T
λy1:T.λ:T.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T
.λy2:T.subst1 (plus (minus d0 (S n)) (S n)) u0 (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
end of h1
(h2)
consider H6
we proved lt n d0
that is equivalent to le (S n) d0
by (le_plus_minus_sym . . previous)
eq nat d0 (plus (minus d0 (S n)) (S n))
end of h2
by (eq_ind_r . . . h1 . h2)
ex3_2
T
T
λy1:T.λ:T.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2)
end of h1
(h2)
suppose H6: eq nat n d0
(H7)
by (eq_ind_r . . . H5 . H6)
drop (S O) n a0 a
end of H7
(H8)
by (eq_ind_r . . . H4 . H6)
csubst1 n u0 c0 a0
end of H8
(H9)
by (eq_ind_r . . . H3 . H6)
getl n c0 (CHead e (Bind Abbr) u0)
end of H9
we proceed by induction on H6 to prove
ex3_2
T
T
λy1:T.λ:T.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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.subst1 n u0 (TLRef n) (lift (S O) n y1)
λ:T.λy2:T.subst1 n u0 (lift (S n) O t) (lift (S O) n y2)
λy1:T.λy2:T.ty3 g a y1 y2
(H10)
by (getl_mono . . . H0 . H9)
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 n c0 (CHead e (Bind Abbr) u0)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
getl n c0 (CHead e (Bind Abbr) u0)
end of H10
(H11)
by (getl_mono . . . H0 . H9)
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 H11
(h1)
(H12)
by (getl_mono . . . H0 . H9)
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 H12
suppose H13: eq C d e
(H14)
consider H12
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 . . . H10 . previous)
getl n c0 (CHead e (Bind Abbr) u)
end of H14
(H15)
consider H12
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 . . . H8 . previous)
csubst1 n u c0 a0
end of H15
consider H12
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
ex3_2
T
T
λy1:T.λ:T.subst1 n u0 (TLRef n) (lift (S O) n y1)
λ:T.λy2:T.subst1 n u0 (lift (S n) O t) (lift (S O) n y2)
λy1:T.λy2:T.ty3 g a y1 y2
case refl_equal : ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.subst1 n u (TLRef n) (lift (S O) n y1)
λ:T.λy2:T.subst1 n u (lift (S n) O t) (lift (S O) n y2)
λy1:T.λy2:T.ty3 g a y1 y2
(H16)
by (eq_ind_r . . . H14 . H13)
getl n c0 (CHead d (Bind Abbr) u)
end of H16
(h1)
(h1)
by (subst0_lref . .)
we proved subst0 n u (TLRef n) (lift (S n) O u)
subst0 n u (TLRef n) (lift (plus (S O) n) O u)
end of h1
(h2)
(h1)
by (le_n .)
we proved le (plus O n) (plus O n)
le n (plus O n)
end of h1
(h2) by (le_O_n .) we proved le O n
by (lift_free . . . . . h1 h2)
eq T (lift (S O) n (lift n O u)) (lift (plus (S O) n) O u)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved subst0 n u (TLRef n) (lift (S O) n (lift n O u))
by (subst1_single . . . . previous)
subst1 n u (TLRef n) (lift (S O) n (lift n O u))
end of h1
(h2)
(h1)
by (subst1_refl . . .)
we proved subst1 n u (lift (S n) O t) (lift (S n) O t)
subst1 n u (lift (S n) O t) (lift (plus (S O) n) O t)
end of h1
(h2)
(h1)
by (le_n .)
we proved le (plus O n) (plus O n)
le n (plus O n)
end of h1
(h2) by (le_O_n .) we proved le O n
by (lift_free . . . . . h1 h2)
eq T (lift (S O) n (lift n O t)) (lift (plus (S O) n) O t)
end of h2
by (eq_ind_r . . . h1 . h2)
subst1 n u (lift (S n) O t) (lift (S O) n (lift n O t))
end of h2
(h3)
by (le_n .)
we proved le n n
by (csubst1_getl_ge . . previous . . . H15 . H16)
we proved getl n a0 (CHead d (Bind Abbr) u)
by (getl_conf_ge_drop . . . . . previous . H7)
we proved drop n O a d
by (ty3_lift . . . . H1 . . . previous)
ty3 g a (lift n O u) (lift n O t)
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
ex3_2
T
T
λy1:T.λ:T.subst1 n u (TLRef n) (lift (S O) n y1)
λ:T.λy2:T.subst1 n u (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.subst1 n u0 (TLRef n) (lift (S O) n y1)
λ:T.λy2:T.subst1 n u0 (lift (S n) O t) (lift (S O) n y2)
λy1:T.λy2:T.ty3 g a y1 y2
eq C d e
→(ex3_2
T
T
λy1:T.λ:T.subst1 n u0 (TLRef n) (lift (S O) n y1)
λ:T.λy2:T.subst1 n u0 (lift (S n) O t) (lift (S O) n y2)
λy1:T.λy2:T.ty3 g a y1 y2)
end of h1
(h2)
consider H11
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)
ex3_2
T
T
λy1:T.λ:T.subst1 n u0 (TLRef n) (lift (S O) n y1)
λ:T.λy2:T.subst1 n u0 (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.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2)
end of h2
(h3)
suppose H6: 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.subst1 d0 u0 (TLRef (S (plus O (minus n (S O))))) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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.subst1 d0 u0 (TLRef (plus (S O) (minus n (S O)))) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (lift (S n) O t) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
(h1)
(h1)
(h1)
by (subst1_refl . . .)
subst1
d0
u0
TLRef (plus (minus n (S O)) (S O))
TLRef (plus (minus n (S O)) (S O))
end of h1
(h2)
by (lt_le_minus . . H6)
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)
subst1
d0
u0
TLRef (plus (minus n (S O)) (S O))
lift (S O) d0 (TLRef (minus n (S O)))
end of h1
(h2)
(h1)
by (subst1_refl . . .)
we proved subst1 d0 u0 (lift (S n) O t) (lift (S n) O t)
subst1 d0 u0 (lift (S n) O t) (lift (plus (S O) n) O t)
end of h1
(h2)
(h1)
consider H6
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)
subst1 d0 u0 (lift (S n) O t) (lift (S O) d0 (lift n O t))
end of h2
(h3)
(h1)
(h1)
consider H6
we proved lt d0 n
that is equivalent to le (S d0) n
by (le_S . . previous)
we proved le (S d0) (S n)
by (le_S_n . . previous)
we proved le d0 n
by (csubst1_getl_ge . . previous . . . H4 . H0)
getl n a0 (CHead d (Bind Abbr) u)
end of h1
(h2)
(h1)
consider H6
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)
le (plus d0 (S O)) n
end of h2
by (getl_drop_conf_ge . . . h1 . . . H5 h2)
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 H6)
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.subst1 d0 u0 (TLRef (plus (minus n (S O)) (S O))) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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.subst1 d0 u0 (TLRef (plus (S O) (minus n (S O)))) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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.subst1 d0 u0 (TLRef (S (plus O (minus n (S O))))) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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 H6)
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.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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 Abbr) u0)
.∀a0:C
.∀H4:csubst1 d0 u0 c0 a0
.∀a:C
.∀H5:drop (S O) d0 a0 a
.ex3_2
T
T
λy1:T.λ:T.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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 Abbr) u0)
.∀a0:C
.∀H4:csubst1 d0 u0 c0 a0
.∀a:C
.∀H5:drop (S O) d0 a0 a
.ex3_2
T
T
λy1:T.λ:T.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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 Abbr) u0)
→∀a0:C
.csubst1 d0 u0 d a0
→∀a:C
.drop (S O) d0 a0 a
→ex3_2 T T λy1:T.λ:T.subst1 d0 u0 u (lift (S O) d0 y1) λ:T.λy2:T.subst1 d0 u0 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 Abbr) u0)
assume a0: C
suppose H4: csubst1 d0 u0 c0 a0
assume a: C
suppose H5: drop (S O) d0 a0 a
(h1)
suppose H6: lt n d0
(H7)
by (minus_x_Sy . . H6)
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 Abbr) u0
case refl_equal : ⇒
the thesis becomes
getl
minus d0 n
CHead d (Bind Abst) u
CHead e (Bind Abbr) u0
consider H6
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 Abbr) u0
getl
S (minus d0 (S n))
CHead d (Bind Abst) u
CHead e (Bind Abbr) u0
end of H7
by (csubst1_getl_lt . . H6 . . . H4 . H0)
we proved ex2 C λe2:C.csubst1 (minus d0 n) u0 (CHead d (Bind Abst) u) e2 λe2:C.getl n a0 e2
we proceed by induction on the previous result to prove
ex3_2
T
T
λy1:T.λ:T.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (lift (S n) O u) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
case ex_intro2 : x:C H8:csubst1 (minus d0 n) u0 (CHead d (Bind Abst) u) x H9:getl n a0 x ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (lift (S n) O u) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
(H10)
by (minus_x_Sy . . H6)
we proved eq nat (minus d0 n) (S (minus d0 (S n)))
we proceed by induction on the previous result to prove csubst1 (S (minus d0 (S n))) u0 (CHead d (Bind Abst) u) x
case refl_equal : ⇒
the thesis becomes the hypothesis H8
csubst1 (S (minus d0 (S n))) u0 (CHead d (Bind Abst) u) x
end of H10
(H11)
consider H10
we proved csubst1 (S (minus d0 (S n))) u0 (CHead d (Bind Abst) u) x
that is equivalent to csubst1 (s (Bind Abst) (minus d0 (S n))) u0 (CHead d (Bind Abst) u) x
by (csubst1_gen_head . . . . . . previous)
ex3_2
T
C
λu2:T.λc2:C.eq C x (CHead c2 (Bind Abst) u2)
λu2:T.λ:C.subst1 (minus d0 (S n)) u0 u u2
λ:T.λc2:C.csubst1 (minus d0 (S n)) u0 d c2
end of H11
we proceed by induction on H11 to prove
ex3_2
T
T
λy1:T.λ:T.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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 H12:eq C x (CHead x1 (Bind Abst) x0) H13:subst1 (minus d0 (S n)) u0 u x0 H14:csubst1 (minus d0 (S n)) u0 d x1 ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (lift (S n) O u) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
(H15)
we proceed by induction on H12 to prove getl n a0 (CHead x1 (Bind Abst) x0)
case refl_equal : ⇒
the thesis becomes the hypothesis H9
getl n a0 (CHead x1 (Bind Abst) x0)
end of H15
(H16)
by (lt_plus_minus . . H6)
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)))) a0 a
case refl_equal : ⇒
the thesis becomes the hypothesis H5
drop (S O) (S (plus n (minus d0 (S n)))) a0 a
end of H16
by (getl_drop_conf_lt . . . . . H15 . . . H16)
we proved
ex3_2
T
C
λv:T.λ:C.eq T x0 (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)) x1 e0
we proceed by induction on the previous result to prove
ex3_2
T
T
λy1:T.λ:T.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (lift (S n) O u) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
case ex3_2_intro : x2:T x3:C H17:eq T x0 (lift (S O) (minus d0 (S n)) x2) H18:getl n a (CHead x3 (Bind Abst) x2) H19:drop (S O) (minus d0 (S n)) x1 x3 ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (lift (S n) O u) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
(H20)
we proceed by induction on H17 to prove subst1 (minus d0 (S n)) u0 u (lift (S O) (minus d0 (S n)) x2)
case refl_equal : ⇒
the thesis becomes the hypothesis H13
subst1 (minus d0 (S n)) u0 u (lift (S O) (minus d0 (S n)) x2)
end of H20
(H21)
by (getl_gen_S . . . . . H7)
we proved
getl
r (Bind Abst) (minus d0 (S n))
d
CHead e (Bind Abbr) u0
that is equivalent to getl (minus d0 (S n)) d (CHead e (Bind Abbr) u0)
by (H2 . . . previous . H14 . H19)
ex3_2
T
T
λy1:T.λ:T.subst1 (minus d0 (S n)) u0 u (lift (S O) (minus d0 (S n)) y1)
λ:T.λy2:T.subst1 (minus d0 (S n)) u0 t (lift (S O) (minus d0 (S n)) y2)
λy1:T.λy2:T.ty3 g x3 y1 y2
end of H21
we proceed by induction on H21 to prove
ex3_2
T
T
λy1:T.λ:T.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (lift (S n) O u) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
case ex3_2_intro : x4:T x5:T H22:subst1 (minus d0 (S n)) u0 u (lift (S O) (minus d0 (S n)) x4) :subst1 (minus d0 (S n)) u0 t (lift (S O) (minus d0 (S n)) x5) H24:ty3 g x3 x4 x5 ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (lift (S n) O u) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
(H25)
by (subst1_confluence_lift . . . . H22 . H20)
we proved eq T x4 x2
we proceed by induction on the previous result to prove ty3 g x3 x2 x5
case refl_equal : ⇒
the thesis becomes the hypothesis H24
ty3 g x3 x2 x5
end of H25
(h1)
(h1)
(h1)
(h1)
by (subst1_refl . . .)
subst1 d0 u0 (TLRef n) (TLRef n)
end of h1
(h2)
by (lift_lref_lt . . . H6)
eq T (lift (S O) d0 (TLRef n)) (TLRef n)
end of h2
by (eq_ind_r . . . h1 . h2)
subst1 d0 u0 (TLRef n) (lift (S O) d0 (TLRef n))
end of h1
(h2)
(h1)
by (le_O_n .)
we proved le O (minus d0 (S n))
by (subst1_lift_ge . . . . . H20 . previous)
subst1
plus (minus d0 (S n)) (S n)
u0
lift (S n) O u
lift (S n) O (lift (S O) (minus d0 (S n)) x2)
end of h1
(h2)
by (le_O_n .)
we proved le O (minus d0 (S n))
by (lift_d . . . . . previous)
eq
T
lift (S O) (plus (S n) (minus d0 (S n))) (lift (S n) O x2)
lift (S n) O (lift (S O) (minus d0 (S n)) x2)
end of h2
by (eq_ind_r . . . h1 . h2)
subst1
plus (minus d0 (S n)) (S n)
u0
lift (S n) O u
lift (S O) (plus (S n) (minus d0 (S n))) (lift (S n) O x2)
end of h2
(h3)
by (ty3_abst . . . . . H18 . H25)
ty3 g a (TLRef n) (lift (S n) O x2)
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
ex3_2
T
T
λy1:T.λ:T.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T
.λy2:T
.subst1
plus (minus d0 (S n)) (S n)
u0
lift (S n) O u
lift (S O) (plus (S n) (minus d0 (S n))) y2
λy1:T.λy2:T.ty3 g a y1 y2
end of h1
(h2)
consider H6
we proved lt n d0
that is equivalent to le (S n) d0
by (le_plus_minus . . previous)
eq nat d0 (plus (S n) (minus d0 (S n)))
end of h2
by (eq_ind_r . . . h1 . h2)
ex3_2
T
T
λy1:T.λ:T.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T
.λy2:T.subst1 (plus (minus d0 (S n)) (S n)) u0 (lift (S n) O u) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
end of h1
(h2)
consider H6
we proved lt n d0
that is equivalent to le (S n) d0
by (le_plus_minus_sym . . previous)
eq nat d0 (plus (minus d0 (S n)) (S n))
end of h2
by (eq_ind_r . . . h1 . h2)
ex3_2
T
T
λy1:T.λ:T.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (lift (S n) O u) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2)
end of h1
(h2)
suppose H6: eq nat n d0
(H9)
by (eq_ind_r . . . H3 . H6)
getl n c0 (CHead e (Bind Abbr) u0)
end of H9
we proceed by induction on H6 to prove
ex3_2
T
T
λy1:T.λ:T.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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.subst1 n u0 (TLRef n) (lift (S O) n y1)
λ:T.λy2:T.subst1 n u0 (lift (S n) O u) (lift (S O) n y2)
λy1:T.λy2:T.ty3 g a y1 y2
(H11)
by (getl_mono . . . H0 . H9)
we proved eq C (CHead d (Bind Abst) u) (CHead e (Bind Abbr) u0)
we proceed by induction on the previous result to prove
<λ:C.Prop>
CASE CHead e (Bind Abbr) 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 Abbr) 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 H11
consider H11
we proved
<λ:C.Prop>
CASE CHead e (Bind Abbr) 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.subst1 n u0 (TLRef n) (lift (S O) n y1)
λ:T.λy2:T.subst1 n u0 (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.subst1 n u0 (TLRef n) (lift (S O) n y1)
λ:T.λy2:T.subst1 n u0 (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.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (lift (S n) O u) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2)
end of h2
(h3)
suppose H6: 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.subst1 d0 u0 (TLRef (S (plus O (minus n (S O))))) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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.subst1 d0 u0 (TLRef (plus (S O) (minus n (S O)))) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (lift (S n) O u) (lift (S O) d0 y2)
λy1:T.λy2:T.ty3 g a y1 y2
(h1)
(h1)
(h1)
by (subst1_refl . . .)
subst1
d0
u0
TLRef (plus (minus n (S O)) (S O))
TLRef (plus (minus n (S O)) (S O))
end of h1
(h2)
by (lt_le_minus . . H6)
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)
subst1
d0
u0
TLRef (plus (minus n (S O)) (S O))
lift (S O) d0 (TLRef (minus n (S O)))
end of h1
(h2)
(h1)
by (subst1_refl . . .)
we proved subst1 d0 u0 (lift (S n) O u) (lift (S n) O u)
subst1 d0 u0 (lift (S n) O u) (lift (plus (S O) n) O u)
end of h1
(h2)
(h1)
consider H6
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)
subst1 d0 u0 (lift (S n) O u) (lift (S O) d0 (lift n O u))
end of h2
(h3)
(h1)
(h1)
consider H6
we proved lt d0 n
that is equivalent to le (S d0) n
by (le_S . . previous)
we proved le (S d0) (S n)
by (le_S_n . . previous)
we proved le d0 n
by (csubst1_getl_ge . . previous . . . H4 . H0)
getl n a0 (CHead d (Bind Abst) u)
end of h1
(h2)
(h1)
consider H6
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)
le (plus d0 (S O)) n
end of h2
by (getl_drop_conf_ge . . . h1 . . . H5 h2)
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 H6)
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.subst1 d0 u0 (TLRef (plus (minus n (S O)) (S O))) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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.subst1 d0 u0 (TLRef (plus (S O) (minus n (S O)))) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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.subst1 d0 u0 (TLRef (S (plus O (minus n (S O))))) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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 H6)
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.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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 Abbr) u0)
.∀a0:C
.∀H4:csubst1 d0 u0 c0 a0
.∀a:C
.∀H5:drop (S O) d0 a0 a
.ex3_2
T
T
λy1:T.λ:T.subst1 d0 u0 (TLRef n) (lift (S O) d0 y1)
λ:T.λy2:T.subst1 d0 u0 (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 :ty3 g c0 u t b:B t3:T t4:T :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 Abbr) u0)
.∀a0:C
.∀H5:csubst1 d u0 c0 a0
.∀a:C
.∀H6:drop (S O) d a0 a
.ex3_2
T
T
λy1:T.λ:T.subst1 d u0 (THead (Bind b) u t3) (lift (S O) d y1)
λ:T.λy2:T.subst1 d u0 (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 Abbr) u0)
→∀a0:C
.csubst1 d u0 c0 a0
→∀a:C
.drop (S O) d a0 a
→ex3_2 T T λy1:T.λ:T.subst1 d u0 u (lift (S O) d y1) λ:T.λy2:T.subst1 d u0 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 Abbr) u0)
→∀a0:C
.csubst1 d u0 (CHead c0 (Bind b) u) a0
→∀a:C
.drop (S O) d a0 a
→ex3_2 T T λy1:T.λ:T.subst1 d u0 t3 (lift (S O) d y1) λ:T.λy2:T.subst1 d u0 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 Abbr) u0)
assume a0: C
suppose H5: csubst1 d u0 c0 a0
assume a: C
suppose H6: drop (S O) d a0 a
(H7)
by (H1 . . . H4 . H5 . H6)
ex3_2 T T λy1:T.λ:T.subst1 d u0 u (lift (S O) d y1) λ:T.λy2:T.subst1 d u0 t (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.subst1 d u0 (THead (Bind b) u t3) (lift (S O) d y1)
λ:T.λy2:T.subst1 d u0 (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 H8:subst1 d u0 u (lift (S O) d x0) :subst1 d u0 t (lift (S O) d x1) H10:ty3 g a x0 x1 ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.subst1 d u0 (THead (Bind b) u t3) (lift (S O) d y1)
λ:T.λy2:T.subst1 d u0 (THead (Bind b) u t4) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
(H11)
(h1)
consider H4
we proved getl d c0 (CHead e (Bind Abbr) u0)
that is equivalent to getl (r (Bind b) d) c0 (CHead e (Bind Abbr) u0)
by (getl_head . . . . previous .)
getl (S d) (CHead c0 (Bind b) u) (CHead e (Bind Abbr) u0)
end of h1
(h2)
by (csubst1_bind . . . . . H8 . . H5)
csubst1 (S d) u0 (CHead c0 (Bind b) u) (CHead a0 (Bind b) (lift (S O) d x0))
end of h2
(h3)
by (drop_skip_bind . . . . H6 . .)
drop
S O
S d
CHead a0 (Bind b) (lift (S O) d x0)
CHead a (Bind b) x0
end of h3
by (H3 . . . h1 . h2 . h3)
ex3_2
T
T
λy1:T.λ:T.subst1 (S d) u0 t3 (lift (S O) (S d) y1)
λ:T.λy2:T.subst1 (S d) u0 t4 (lift (S O) (S d) y2)
λy1:T.λy2:T.ty3 g (CHead a (Bind b) x0) y1 y2
end of H11
we proceed by induction on H11 to prove
ex3_2
T
T
λy1:T.λ:T.subst1 d u0 (THead (Bind b) u t3) (lift (S O) d y1)
λ:T.λy2:T.subst1 d u0 (THead (Bind b) u t4) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
case ex3_2_intro : x2:T x3:T H12:subst1 (S d) u0 t3 (lift (S O) (S d) x2) H13:subst1 (S d) u0 t4 (lift (S O) (S d) x3) H14:ty3 g (CHead a (Bind b) x0) x2 x3 ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.subst1 d u0 (THead (Bind b) u t3) (lift (S O) d y1)
λ:T.λy2:T.subst1 d u0 (THead (Bind b) u t4) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
(h1)
(h1)
consider H12
we proved subst1 (S d) u0 t3 (lift (S O) (S d) x2)
that is equivalent to subst1 (s (Bind b) d) u0 t3 (lift (S O) (S d) x2)
by (subst1_head . . . . H8 . . . previous)
subst1
d
u0
THead (Bind b) u t3
THead (Bind b) (lift (S O) d x0) (lift (S O) (S d) x2)
end of h1
(h2)
by (lift_bind . . . . .)
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)
end of h2
by (eq_ind_r . . . h1 . h2)
subst1 d u0 (THead (Bind b) u t3) (lift (S O) d (THead (Bind b) x0 x2))
end of h1
(h2)
(h1)
consider H13
we proved subst1 (S d) u0 t4 (lift (S O) (S d) x3)
that is equivalent to subst1 (s (Bind b) d) u0 t4 (lift (S O) (S d) x3)
by (subst1_head . . . . H8 . . . previous)
subst1
d
u0
THead (Bind b) u t4
THead (Bind b) (lift (S O) d x0) (lift (S O) (S d) x3)
end of h1
(h2)
by (lift_bind . . . . .)
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)
end of h2
by (eq_ind_r . . . h1 . h2)
subst1 d u0 (THead (Bind b) u t4) (lift (S O) d (THead (Bind b) x0 x3))
end of h2
(h3)
by (ty3_bind . . . . H10 . . . H14)
ty3 g a (THead (Bind b) x0 x2) (THead (Bind b) x0 x3)
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
ex3_2
T
T
λy1:T.λ:T.subst1 d u0 (THead (Bind b) u t3) (lift (S O) d y1)
λ:T.λy2:T.subst1 d u0 (THead (Bind b) u t4) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
ex3_2
T
T
λy1:T.λ:T.subst1 d u0 (THead (Bind b) u t3) (lift (S O) d y1)
λ:T.λy2:T.subst1 d u0 (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.subst1 d u0 (THead (Bind b) u t3) (lift (S O) d y1)
λ:T.λy2:T.subst1 d u0 (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 Abbr) u0)
.∀a0:C
.∀H5:csubst1 d u0 c0 a0
.∀a:C
.∀H6:drop (S O) d a0 a
.ex3_2
T
T
λy1:T.λ:T.subst1 d u0 (THead (Bind b) u t3) (lift (S O) d y1)
λ:T.λy2:T.subst1 d u0 (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 :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 Abbr) u0)
.∀a0:C
.∀H5:csubst1 d u0 c0 a0
.∀a:C
.∀H6:drop (S O) d a0 a
.ex3_2
T
T
λy1:T.λ:T.subst1 d u0 (THead (Flat Appl) w v) (lift (S O) d y1)
λ:T
.λy2:T
.subst1
d
u0
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 Abbr) u0)
→∀a0:C
.csubst1 d u0 c0 a0
→∀a:C
.drop (S O) d a0 a
→ex3_2 T T λy1:T.λ:T.subst1 d u0 w (lift (S O) d y1) λ:T.λy2:T.subst1 d u0 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 Abbr) u0)
→∀a0:C
.csubst1 d u0 c0 a0
→∀a:C
.drop (S O) d a0 a
→(ex3_2
T
T
λy1:T.λ:T.subst1 d u0 v (lift (S O) d y1)
λ:T.λy2:T.subst1 d u0 (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 Abbr) u0)
assume a0: C
suppose H5: csubst1 d u0 c0 a0
assume a: C
suppose H6: drop (S O) d a0 a
(H7)
by (H3 . . . H4 . H5 . H6)
ex3_2
T
T
λy1:T.λ:T.subst1 d u0 v (lift (S O) d y1)
λ:T.λy2:T.subst1 d u0 (THead (Bind Abst) u t) (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.subst1 d u0 (THead (Flat Appl) w v) (lift (S O) d y1)
λ:T
.λy2:T
.subst1
d
u0
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 H8:subst1 d u0 v (lift (S O) d x0) H9:subst1 d u0 (THead (Bind Abst) u t) (lift (S O) d x1) H10:ty3 g a x0 x1 ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.subst1 d u0 (THead (Flat Appl) w v) (lift (S O) d y1)
λ:T
.λy2:T
.subst1
d
u0
THead (Flat Appl) w (THead (Bind Abst) u t)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
(H11)
by (H1 . . . H4 . H5 . H6)
ex3_2 T T λy1:T.λ:T.subst1 d u0 w (lift (S O) d y1) λ:T.λy2:T.subst1 d u0 u (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
end of H11
we proceed by induction on H11 to prove
ex3_2
T
T
λy1:T.λ:T.subst1 d u0 (THead (Flat Appl) w v) (lift (S O) d y1)
λ:T
.λy2:T
.subst1
d
u0
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 H12:subst1 d u0 w (lift (S O) d x2) H13:subst1 d u0 u (lift (S O) d x3) H14:ty3 g a x2 x3 ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.subst1 d u0 (THead (Flat Appl) w v) (lift (S O) d y1)
λ:T
.λy2:T
.subst1
d
u0
THead (Flat Appl) w (THead (Bind Abst) u t)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
(H_x)
by (subst1_gen_head . . . . . . H9)
ex3_2
T
T
λu2:T.λt2:T.eq T (lift (S O) d x1) (THead (Bind Abst) u2 t2)
λu2:T.λ:T.subst1 d u0 u u2
λ:T.λt2:T.subst1 (s (Bind Abst) d) u0 t t2
end of H_x
(H15) consider H_x
consider H15
we proved
ex3_2
T
T
λu2:T.λt2:T.eq T (lift (S O) d x1) (THead (Bind Abst) u2 t2)
λu2:T.λ:T.subst1 d u0 u u2
λ:T.λt2:T.subst1 (s (Bind Abst) d) u0 t t2
that is equivalent to
ex3_2
T
T
λu2:T.λt3:T.eq T (lift (S O) d x1) (THead (Bind Abst) u2 t3)
λu2:T.λ:T.subst1 d u0 u u2
λ:T.λt3:T.subst1 (S d) u0 t t3
we proceed by induction on the previous result to prove
ex3_2
T
T
λy1:T.λ:T.subst1 d u0 (THead (Flat Appl) w v) (lift (S O) d y1)
λ:T
.λy2:T
.subst1
d
u0
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 : x4:T x5:T H16:eq T (lift (S O) d x1) (THead (Bind Abst) x4 x5) H17:subst1 d u0 u x4 H18:subst1 (S d) u0 t x5 ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.subst1 d u0 (THead (Flat Appl) w v) (lift (S O) d y1)
λ:T
.λy2:T
.subst1
d
u0
THead (Flat Appl) w (THead (Bind Abst) u t)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
(H19)
by (sym_eq . . . H16)
eq T (THead (Bind Abst) x4 x5) (lift (S O) d x1)
end of H19
by (lift_gen_bind . . . . . . H19)
we proved
ex3_2
T
T
λy:T.λz:T.eq T x1 (THead (Bind Abst) y z)
λy:T.λ:T.eq T x4 (lift (S O) d y)
λ:T.λz:T.eq T x5 (lift (S O) (S d) z)
we proceed by induction on the previous result to prove
ex3_2
T
T
λy1:T.λ:T.subst1 d u0 (THead (Flat Appl) w v) (lift (S O) d y1)
λ:T
.λy2:T
.subst1
d
u0
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 : x6:T x7:T H20:eq T x1 (THead (Bind Abst) x6 x7) H21:eq T x4 (lift (S O) d x6) H22:eq T x5 (lift (S O) (S d) x7) ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.subst1 d u0 (THead (Flat Appl) w v) (lift (S O) d y1)
λ:T
.λy2:T
.subst1
d
u0
THead (Flat Appl) w (THead (Bind Abst) u t)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
(H23)
we proceed by induction on H22 to prove subst1 (S d) u0 t (lift (S O) (S d) x7)
case refl_equal : ⇒
the thesis becomes the hypothesis H18
subst1 (S d) u0 t (lift (S O) (S d) x7)
end of H23
(H24)
we proceed by induction on H21 to prove subst1 d u0 u (lift (S O) d x6)
case refl_equal : ⇒
the thesis becomes the hypothesis H17
subst1 d u0 u (lift (S O) d x6)
end of H24
(H25)
we proceed by induction on H20 to prove ty3 g a x0 (THead (Bind Abst) x6 x7)
case refl_equal : ⇒
the thesis becomes the hypothesis H10
ty3 g a x0 (THead (Bind Abst) x6 x7)
end of H25
(H26)
by (subst1_confluence_lift . . . . H24 . H13)
we proved eq T x6 x3
we proceed by induction on the previous result to prove ty3 g a x0 (THead (Bind Abst) x3 x7)
case refl_equal : ⇒
the thesis becomes the hypothesis H25
ty3 g a x0 (THead (Bind Abst) x3 x7)
end of H26
(h1)
(h1)
consider H8
we proved subst1 d u0 v (lift (S O) d x0)
that is equivalent to subst1 (s (Flat Appl) d) u0 v (lift (S O) d x0)
by (subst1_head . . . . H12 . . . previous)
subst1
d
u0
THead (Flat Appl) w v
THead (Flat Appl) (lift (S O) d x2) (lift (S O) d x0)
end of h1
(h2)
by (lift_flat . . . . .)
eq
T
lift (S O) d (THead (Flat Appl) x2 x0)
THead (Flat Appl) (lift (S O) d x2) (lift (S O) d x0)
end of h2
by (eq_ind_r . . . h1 . h2)
subst1
d
u0
THead (Flat Appl) w v
lift (S O) d (THead (Flat Appl) x2 x0)
end of h1
(h2)
(h1)
(h1)
(h1)
consider H13
we proved subst1 d u0 u (lift (S O) d x3)
subst1 (s (Flat Appl) d) u0 u (lift (S O) d x3)
end of h1
(h2)
consider H23
we proved subst1 (S d) u0 t (lift (S O) (S d) x7)
subst1 (s (Bind Abst) (s (Flat Appl) d)) u0 t (lift (S O) (S d) x7)
end of h2
by (subst1_head . . . . h1 . . . h2)
subst1
s (Flat Appl) d
u0
THead (Bind Abst) u t
THead (Bind Abst) (lift (S O) d x3) (lift (S O) (S d) x7)
end of h1
(h2)
by (lift_bind . . . . .)
eq
T
lift (S O) d (THead (Bind Abst) x3 x7)
THead (Bind Abst) (lift (S O) d x3) (lift (S O) (S d) x7)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
subst1
s (Flat Appl) d
u0
THead (Bind Abst) u t
lift (S O) d (THead (Bind Abst) x3 x7)
by (subst1_head . . . . H12 . . . previous)
subst1
d
u0
THead (Flat Appl) w (THead (Bind Abst) u t)
THead
Flat Appl
lift (S O) d x2
lift (S O) d (THead (Bind Abst) x3 x7)
end of h1
(h2)
by (lift_flat . . . . .)
eq
T
lift (S O) d (THead (Flat Appl) x2 (THead (Bind Abst) x3 x7))
THead
Flat Appl
lift (S O) d x2
lift (S O) d (THead (Bind Abst) x3 x7)
end of h2
by (eq_ind_r . . . h1 . h2)
subst1
d
u0
THead (Flat Appl) w (THead (Bind Abst) u t)
lift (S O) d (THead (Flat Appl) x2 (THead (Bind Abst) x3 x7))
end of h2
(h3)
by (ty3_appl . . . . H14 . . H26)
ty3
g
a
THead (Flat Appl) x2 x0
THead (Flat Appl) x2 (THead (Bind Abst) x3 x7)
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
ex3_2
T
T
λy1:T.λ:T.subst1 d u0 (THead (Flat Appl) w v) (lift (S O) d y1)
λ:T
.λy2:T
.subst1
d
u0
THead (Flat Appl) w (THead (Bind Abst) u t)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
ex3_2
T
T
λy1:T.λ:T.subst1 d u0 (THead (Flat Appl) w v) (lift (S O) d y1)
λ:T
.λy2:T
.subst1
d
u0
THead (Flat Appl) w (THead (Bind Abst) u t)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
ex3_2
T
T
λy1:T.λ:T.subst1 d u0 (THead (Flat Appl) w v) (lift (S O) d y1)
λ:T
.λy2:T
.subst1
d
u0
THead (Flat Appl) w (THead (Bind Abst) u t)
lift (S O) d y2
λy1:T.λy2:T.ty3 g a y1 y2
ex3_2
T
T
λy1:T.λ:T.subst1 d u0 (THead (Flat Appl) w v) (lift (S O) d y1)
λ:T
.λy2:T
.subst1
d
u0
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.subst1 d u0 (THead (Flat Appl) w v) (lift (S O) d y1)
λ:T
.λy2:T
.subst1
d
u0
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 Abbr) u0)
.∀a0:C
.∀H5:csubst1 d u0 c0 a0
.∀a:C
.∀H6:drop (S O) d a0 a
.ex3_2
T
T
λy1:T.λ:T.subst1 d u0 (THead (Flat Appl) w v) (lift (S O) d y1)
λ:T
.λy2:T
.subst1
d
u0
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 :ty3 g c0 t3 t4 t0:T :ty3 g c0 t4 t0 ⇒
the thesis becomes
∀e:C
.∀u:T
.∀d:nat
.∀H4:getl d c0 (CHead e (Bind Abbr) u)
.∀a0:C
.∀H5:csubst1 d u c0 a0
.∀a:C
.∀H6:drop (S O) d a0 a
.ex3_2
T
T
λy1:T.λ:T.subst1 d u (THead (Flat Cast) t4 t3) (lift (S O) d y1)
λ:T.λy2:T.subst1 d u (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 Abbr) u)
→∀a0:C
.csubst1 d u c0 a0
→∀a:C
.drop (S O) d a0 a
→ex3_2 T T λy1:T.λ:T.subst1 d u t3 (lift (S O) d y1) λ:T.λy2:T.subst1 d u 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 Abbr) u)
→∀a0:C
.csubst1 d u c0 a0
→∀a:C
.drop (S O) d a0 a
→ex3_2 T T λy1:T.λ:T.subst1 d u t4 (lift (S O) d y1) λ:T.λy2:T.subst1 d u 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 Abbr) u)
assume a0: C
suppose H5: csubst1 d u c0 a0
assume a: C
suppose H6: drop (S O) d a0 a
(H7)
by (H3 . . . H4 . H5 . H6)
ex3_2 T T λy1:T.λ:T.subst1 d u t4 (lift (S O) d y1) λ:T.λy2:T.subst1 d u t0 (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.subst1 d u (THead (Flat Cast) t4 t3) (lift (S O) d y1)
λ:T.λy2:T.subst1 d u (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 H8:subst1 d u t4 (lift (S O) d x0) H9:subst1 d u t0 (lift (S O) d x1) H10:ty3 g a x0 x1 ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.subst1 d u (THead (Flat Cast) t4 t3) (lift (S O) d y1)
λ:T.λy2:T.subst1 d u (THead (Flat Cast) t0 t4) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
(H11)
by (H1 . . . H4 . H5 . H6)
ex3_2 T T λy1:T.λ:T.subst1 d u t3 (lift (S O) d y1) λ:T.λy2:T.subst1 d u t4 (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
end of H11
we proceed by induction on H11 to prove
ex3_2
T
T
λy1:T.λ:T.subst1 d u (THead (Flat Cast) t4 t3) (lift (S O) d y1)
λ:T.λy2:T.subst1 d u (THead (Flat Cast) t0 t4) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
case ex3_2_intro : x2:T x3:T H12:subst1 d u t3 (lift (S O) d x2) H13:subst1 d u t4 (lift (S O) d x3) H14:ty3 g a x2 x3 ⇒
the thesis becomes
ex3_2
T
T
λy1:T.λ:T.subst1 d u (THead (Flat Cast) t4 t3) (lift (S O) d y1)
λ:T.λy2:T.subst1 d u (THead (Flat Cast) t0 t4) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
(H15)
by (subst1_confluence_lift . . . . H13 . H8)
we proved eq T x3 x0
we proceed by induction on the previous result to prove ty3 g a x2 x0
case refl_equal : ⇒
the thesis becomes the hypothesis H14
ty3 g a x2 x0
end of H15
(h1)
(h1)
consider H12
we proved subst1 d u t3 (lift (S O) d x2)
that is equivalent to subst1 (s (Flat Cast) d) u t3 (lift (S O) d x2)
by (subst1_head . . . . H8 . . . previous)
subst1
d
u
THead (Flat Cast) t4 t3
THead (Flat Cast) (lift (S O) d x0) (lift (S O) d x2)
end of h1
(h2)
by (lift_flat . . . . .)
eq
T
lift (S O) d (THead (Flat Cast) x0 x2)
THead (Flat Cast) (lift (S O) d x0) (lift (S O) d x2)
end of h2
by (eq_ind_r . . . h1 . h2)
subst1
d
u
THead (Flat Cast) t4 t3
lift (S O) d (THead (Flat Cast) x0 x2)
end of h1
(h2)
(h1)
consider H8
we proved subst1 d u t4 (lift (S O) d x0)
that is equivalent to subst1 (s (Flat Cast) d) u t4 (lift (S O) d x0)
by (subst1_head . . . . H9 . . . previous)
subst1
d
u
THead (Flat Cast) t0 t4
THead (Flat Cast) (lift (S O) d x1) (lift (S O) d x0)
end of h1
(h2)
by (lift_flat . . . . .)
eq
T
lift (S O) d (THead (Flat Cast) x1 x0)
THead (Flat Cast) (lift (S O) d x1) (lift (S O) d x0)
end of h2
by (eq_ind_r . . . h1 . h2)
subst1
d
u
THead (Flat Cast) t0 t4
lift (S O) d (THead (Flat Cast) x1 x0)
end of h2
(h3)
by (ty3_cast . . . . H15 . H10)
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.subst1 d u (THead (Flat Cast) t4 t3) (lift (S O) d y1)
λ:T.λy2:T.subst1 d u (THead (Flat Cast) t0 t4) (lift (S O) d y2)
λy1:T.λy2:T.ty3 g a y1 y2
ex3_2
T
T
λy1:T.λ:T.subst1 d u (THead (Flat Cast) t4 t3) (lift (S O) d y1)
λ:T.λy2:T.subst1 d u (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.subst1 d u (THead (Flat Cast) t4 t3) (lift (S O) d y1)
λ:T.λy2:T.subst1 d u (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 Abbr) u)
.∀a0:C
.∀H5:csubst1 d u c0 a0
.∀a:C
.∀H6:drop (S O) d a0 a
.ex3_2
T
T
λy1:T.λ:T.subst1 d u (THead (Flat Cast) t4 t3) (lift (S O) d y1)
λ:T.λy2:T.subst1 d u (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 Abbr) u)
→∀a0:C
.csubst1 d u c a0
→∀a:C
.drop (S O) d a0 a
→ex3_2 T T λy1:T.λ:T.subst1 d u t1 (lift (S O) d y1) λ:T.λy2:T.subst1 d u 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 Abbr) u)
→∀a0:C
.csubst1 d u c a0
→∀a:C
.drop (S O) d a0 a
→ex3_2 T T λy1:T.λ:T.subst1 d u t1 (lift (S O) d y1) λ:T.λy2:T.subst1 d u t2 (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2