DEFINITION csubt_drop_abst()
TYPE =
∀g:G
.∀n:nat
.∀c1:C
.∀c2:C
.csubt g c1 c2
→∀d1:C
.∀t:T
.drop n O c1 (CHead d1 (Bind Abst) t)
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop n O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop n O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
BODY =
assume g: G
assume n: nat
we proceed by induction on n to prove
∀c1:C
.∀c2:C
.csubt g c1 c2
→∀d1:C
.∀t:T
.drop n O c1 (CHead d1 (Bind Abst) t)
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop n O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop n O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
case O : ⇒
the thesis becomes
∀c1:C
.∀c2:C
.csubt g c1 c2
→∀d1:C
.∀t:T
.drop O O c1 (CHead d1 (Bind Abst) t)
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop O O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop O O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
assume c1: C
assume c2: C
suppose H: csubt g c1 c2
assume d1: C
assume t: T
suppose H0: drop O O c1 (CHead d1 (Bind Abst) t)
(H1)
by (drop_gen_refl . . H0)
we proved eq C c1 (CHead d1 (Bind Abst) t)
we proceed by induction on the previous result to prove csubt g (CHead d1 (Bind Abst) t) c2
case refl_equal : ⇒
the thesis becomes the hypothesis H
csubt g (CHead d1 (Bind Abst) t) c2
end of H1
(H2)
by (csubt_gen_abst . . . . H1)
or
ex2 C λe2:C.eq C c2 (CHead e2 (Bind Abst) t) λe2:C.csubt g d1 e2
ex4_2
C
T
λe2:C.λv2:T.eq C c2 (CHead e2 (Bind Abbr) v2)
λe2:C.λ:T.csubt g d1 e2
λ:C.λv2:T.ty3 g d1 v2 t
λe2:C.λv2:T.ty3 g e2 v2 t
end of H2
we proceed by induction on H2 to prove
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop O O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop O O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
case or_introl : H3:ex2 C λe2:C.eq C c2 (CHead e2 (Bind Abst) t) λe2:C.csubt g d1 e2 ⇒
the thesis becomes
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop O O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop O O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
we proceed by induction on H3 to prove
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop O O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop O O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
case ex_intro2 : x:C H4:eq C c2 (CHead x (Bind Abst) t) H5:csubt g d1 x ⇒
the thesis becomes
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop O O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop O O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
by (drop_refl .)
we proved drop O O (CHead x (Bind Abst) t) (CHead x (Bind Abst) t)
by (ex_intro2 . . . . H5 previous)
we proved
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop O O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) t)
by (or_introl . . previous)
we proved
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop O O (CHead x (Bind Abst) t) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop O O (CHead x (Bind Abst) t) (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
by (eq_ind_r . . . previous . H4)
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop O O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop O O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop O O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop O O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
case or_intror : H3:ex4_2 C T λe2:C.λv2:T.eq C c2 (CHead e2 (Bind Abbr) v2) λe2:C.λ:T.csubt g d1 e2 λ:C.λv2:T.ty3 g d1 v2 t λe2:C.λv2:T.ty3 g e2 v2 t ⇒
the thesis becomes
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop O O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop O O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
we proceed by induction on H3 to prove
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop O O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop O O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
case ex4_2_intro : x0:C x1:T H4:eq C c2 (CHead x0 (Bind Abbr) x1) H5:csubt g d1 x0 H6:ty3 g d1 x1 t H7:ty3 g x0 x1 t ⇒
the thesis becomes
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop O O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop O O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
by (drop_refl .)
we proved drop O O (CHead x0 (Bind Abbr) x1) (CHead x0 (Bind Abbr) x1)
by (ex4_2_intro . . . . . . . . H5 previous H6 H7)
we proved
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop O O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
by (or_intror . . previous)
we proved
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop O O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop O O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
by (eq_ind_r . . . previous . H4)
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop O O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop O O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop O O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop O O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
we proved
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop O O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop O O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
∀c1:C
.∀c2:C
.csubt g c1 c2
→∀d1:C
.∀t:T
.drop O O c1 (CHead d1 (Bind Abst) t)
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop O O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop O O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
case S : n0:nat ⇒
the thesis becomes
∀c1:C
.∀c2:C
.∀H0:csubt g c1 c2
.∀d1:C
.∀t:T
.drop (S n0) O c1 (CHead d1 (Bind Abst) t)
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
(H) by induction hypothesis we know
∀c1:C
.∀c2:C
.csubt g c1 c2
→∀d1:C
.∀t:T
.drop n0 O c1 (CHead d1 (Bind Abst) t)
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop n0 O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop n0 O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
assume c1: C
assume c2: C
suppose H0: csubt g c1 c2
we proceed by induction on H0 to prove
∀d1:C
.∀t:T
.drop (S n0) O c1 (CHead d1 (Bind Abst) t)
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
case csubt_sort : n1:nat ⇒
the thesis becomes
∀d1:C
.∀t:T
.∀H1:drop (S n0) O (CSort n1) (CHead d1 (Bind Abst) t)
.or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O (CSort n1) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O (CSort n1) (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
assume d1: C
assume t: T
suppose H1: drop (S n0) O (CSort n1) (CHead d1 (Bind Abst) t)
by (drop_gen_sort . . . . H1)
we proved
and3
eq C (CHead d1 (Bind Abst) t) (CSort n1)
eq nat (S n0) O
eq nat O O
we proceed by induction on the previous result to prove
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O (CSort n1) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O (CSort n1) (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
case and3_intro : :eq C (CHead d1 (Bind Abst) t) (CSort n1) H3:eq nat (S n0) O :eq nat O O ⇒
the thesis becomes
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O (CSort n1) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O (CSort n1) (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
(H5)
we proceed by induction on H3 to prove <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
case refl_equal : ⇒
the thesis becomes <λ:nat.Prop> CASE S n0 OF O⇒False | S ⇒True
consider I
we proved True
<λ:nat.Prop> CASE S n0 OF O⇒False | S ⇒True
<λ:nat.Prop> CASE O OF O⇒False | S ⇒True
end of H5
consider H5
we proved <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O (CSort n1) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O (CSort n1) (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O (CSort n1) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O (CSort n1) (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
we proved
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O (CSort n1) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O (CSort n1) (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
∀d1:C
.∀t:T
.∀H1:drop (S n0) O (CSort n1) (CHead d1 (Bind Abst) t)
.or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O (CSort n1) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O (CSort n1) (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
case csubt_head ⇒
we need to prove
∀c0:C
.∀c3:C
.csubt g c0 c3
→(∀d1:C
.∀t:T
.drop (S n0) O c0 (CHead d1 (Bind Abst) t)
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O c3 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O c3 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
→∀k:K
.∀u:T
.∀d1:C
.∀t:T
.drop (S n0) O (CHead c0 k u) (CHead d1 (Bind Abst) t)
→(or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 k u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 k u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t))
assume c0: C
assume c3: C
suppose H1: csubt g c0 c3
suppose H2:
∀d1:C
.∀t:T
.drop (S n0) O c0 (CHead d1 (Bind Abst) t)
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O c3 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O c3 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
assume k: K
we proceed by induction on k to prove
∀u:T
.∀d1:C
.∀t:T
.drop (S n0) O (CHead c0 k u) (CHead d1 (Bind Abst) t)
→(or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 k u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 k u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t)
case Bind : b:B ⇒
the thesis becomes
∀u:T
.∀d1:C
.∀t:T
.∀H3:drop (S n0) O (CHead c0 (Bind b) u) (CHead d1 (Bind Abst) t)
.or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
assume u: T
assume d1: C
assume t: T
suppose H3: drop (S n0) O (CHead c0 (Bind b) u) (CHead d1 (Bind Abst) t)
by (drop_gen_drop . . . . . H3)
we proved drop (r (Bind b) n0) O c0 (CHead d1 (Bind Abst) t)
that is equivalent to drop n0 O c0 (CHead d1 (Bind Abst) t)
by (H . . H1 . . previous)
we proved
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop n0 O c3 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop n0 O c3 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
we proceed by induction on the previous result to prove
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
case or_introl : H4:ex2 C λd2:C.csubt g d1 d2 λd2:C.drop n0 O c3 (CHead d2 (Bind Abst) t) ⇒
the thesis becomes
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
we proceed by induction on H4 to prove
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
case ex_intro2 : x:C H5:csubt g d1 x H6:drop n0 O c3 (CHead x (Bind Abst) t) ⇒
the thesis becomes
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
consider H6
we proved drop n0 O c3 (CHead x (Bind Abst) t)
that is equivalent to drop (r (Bind b) n0) O c3 (CHead x (Bind Abst) t)
by (drop_drop . . . . previous .)
we proved drop (S n0) O (CHead c3 (Bind b) u) (CHead x (Bind Abst) t)
by (ex_intro2 . . . . H5 previous)
we proved
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abst) t)
by (or_introl . . previous)
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
case or_intror : H4:ex4_2 C T λd2:C.λ:T.csubt g d1 d2 λd2:C.λu0:T.drop n0 O c3 (CHead d2 (Bind Abbr) u0) λ:C.λu0:T.ty3 g d1 u0 t λd2:C.λu0:T.ty3 g d2 u0 t ⇒
the thesis becomes
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
we proceed by induction on H4 to prove
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
case ex4_2_intro : x0:C x1:T H5:csubt g d1 x0 H6:drop n0 O c3 (CHead x0 (Bind Abbr) x1) H7:ty3 g d1 x1 t H8:ty3 g x0 x1 t ⇒
the thesis becomes
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
consider H6
we proved drop n0 O c3 (CHead x0 (Bind Abbr) x1)
that is equivalent to drop (r (Bind b) n0) O c3 (CHead x0 (Bind Abbr) x1)
by (drop_drop . . . . previous .)
we proved drop (S n0) O (CHead c3 (Bind b) u) (CHead x0 (Bind Abbr) x1)
by (ex4_2_intro . . . . . . . . H5 previous H7 H8)
we proved
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
by (or_intror . . previous)
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
we proved
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
∀u:T
.∀d1:C
.∀t:T
.∀H3:drop (S n0) O (CHead c0 (Bind b) u) (CHead d1 (Bind Abst) t)
.or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
case Flat : f:F ⇒
the thesis becomes
∀u:T
.∀d1:C
.∀t:T
.∀H3:drop (S n0) O (CHead c0 (Flat f) u) (CHead d1 (Bind Abst) t)
.or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
assume u: T
assume d1: C
assume t: T
suppose H3: drop (S n0) O (CHead c0 (Flat f) u) (CHead d1 (Bind Abst) t)
by (drop_gen_drop . . . . . H3)
we proved drop (r (Flat f) n0) O c0 (CHead d1 (Bind Abst) t)
that is equivalent to drop (S n0) O c0 (CHead d1 (Bind Abst) t)
by (H2 . . previous)
we proved
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O c3 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O c3 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
we proceed by induction on the previous result to prove
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
case or_introl : H4:ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O c3 (CHead d2 (Bind Abst) t) ⇒
the thesis becomes
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
we proceed by induction on H4 to prove
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
case ex_intro2 : x:C H5:csubt g d1 x H6:drop (S n0) O c3 (CHead x (Bind Abst) t) ⇒
the thesis becomes
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
consider H6
we proved drop (S n0) O c3 (CHead x (Bind Abst) t)
that is equivalent to drop (r (Flat f) n0) O c3 (CHead x (Bind Abst) t)
by (drop_drop . . . . previous .)
we proved drop (S n0) O (CHead c3 (Flat f) u) (CHead x (Bind Abst) t)
by (ex_intro2 . . . . H5 previous)
we proved
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abst) t)
by (or_introl . . previous)
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
case or_intror : H4:ex4_2 C T λd2:C.λ:T.csubt g d1 d2 λd2:C.λu0:T.drop (S n0) O c3 (CHead d2 (Bind Abbr) u0) λ:C.λu0:T.ty3 g d1 u0 t λd2:C.λu0:T.ty3 g d2 u0 t ⇒
the thesis becomes
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
we proceed by induction on H4 to prove
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
case ex4_2_intro : x0:C x1:T H5:csubt g d1 x0 H6:drop (S n0) O c3 (CHead x0 (Bind Abbr) x1) H7:ty3 g d1 x1 t H8:ty3 g x0 x1 t ⇒
the thesis becomes
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
consider H6
we proved drop (S n0) O c3 (CHead x0 (Bind Abbr) x1)
that is equivalent to drop (r (Flat f) n0) O c3 (CHead x0 (Bind Abbr) x1)
by (drop_drop . . . . previous .)
we proved drop (S n0) O (CHead c3 (Flat f) u) (CHead x0 (Bind Abbr) x1)
by (ex4_2_intro . . . . . . . . H5 previous H7 H8)
we proved
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
by (or_intror . . previous)
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
we proved
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
∀u:T
.∀d1:C
.∀t:T
.∀H3:drop (S n0) O (CHead c0 (Flat f) u) (CHead d1 (Bind Abst) t)
.or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Flat f) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t
we proved
∀u:T
.∀d1:C
.∀t:T
.drop (S n0) O (CHead c0 k u) (CHead d1 (Bind Abst) t)
→(or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 k u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 k u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t)
∀c0:C
.∀c3:C
.csubt g c0 c3
→(∀d1:C
.∀t:T
.drop (S n0) O c0 (CHead d1 (Bind Abst) t)
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O c3 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O c3 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
→∀k:K
.∀u:T
.∀d1:C
.∀t:T
.drop (S n0) O (CHead c0 k u) (CHead d1 (Bind Abst) t)
→(or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 k u) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 k u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t
λd2:C.λu0:T.ty3 g d2 u0 t))
case csubt_void : c0:C c3:C H1:csubt g c0 c3 b:B :not (eq B b Void) u1:T u2:T ⇒
the thesis becomes
∀d1:C
.∀t:T
.∀H4:drop (S n0) O (CHead c0 (Bind Void) u1) (CHead d1 (Bind Abst) t)
.or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
() by induction hypothesis we know
∀d1:C
.∀t:T
.drop (S n0) O c0 (CHead d1 (Bind Abst) t)
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O c3 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O c3 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
assume d1: C
assume t: T
suppose H4: drop (S n0) O (CHead c0 (Bind Void) u1) (CHead d1 (Bind Abst) t)
by (drop_gen_drop . . . . . H4)
we proved drop (r (Bind Void) n0) O c0 (CHead d1 (Bind Abst) t)
that is equivalent to drop n0 O c0 (CHead d1 (Bind Abst) t)
by (H . . H1 . . previous)
we proved
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop n0 O c3 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop n0 O c3 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
we proceed by induction on the previous result to prove
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
case or_introl : H5:ex2 C λd2:C.csubt g d1 d2 λd2:C.drop n0 O c3 (CHead d2 (Bind Abst) t) ⇒
the thesis becomes
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
we proceed by induction on H5 to prove
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
case ex_intro2 : x:C H6:csubt g d1 x H7:drop n0 O c3 (CHead x (Bind Abst) t) ⇒
the thesis becomes
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
consider H7
we proved drop n0 O c3 (CHead x (Bind Abst) t)
that is equivalent to drop (r (Bind b) n0) O c3 (CHead x (Bind Abst) t)
by (drop_drop . . . . previous .)
we proved drop (S n0) O (CHead c3 (Bind b) u2) (CHead x (Bind Abst) t)
by (ex_intro2 . . . . H6 previous)
we proved
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abst) t)
by (or_introl . . previous)
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
case or_intror : H5:ex4_2 C T λd2:C.λ:T.csubt g d1 d2 λd2:C.λu:T.drop n0 O c3 (CHead d2 (Bind Abbr) u) λ:C.λu:T.ty3 g d1 u t λd2:C.λu:T.ty3 g d2 u t ⇒
the thesis becomes
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
we proceed by induction on H5 to prove
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
case ex4_2_intro : x0:C x1:T H6:csubt g d1 x0 H7:drop n0 O c3 (CHead x0 (Bind Abbr) x1) H8:ty3 g d1 x1 t H9:ty3 g x0 x1 t ⇒
the thesis becomes
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
consider H7
we proved drop n0 O c3 (CHead x0 (Bind Abbr) x1)
that is equivalent to drop (r (Bind b) n0) O c3 (CHead x0 (Bind Abbr) x1)
by (drop_drop . . . . previous .)
we proved drop (S n0) O (CHead c3 (Bind b) u2) (CHead x0 (Bind Abbr) x1)
by (ex4_2_intro . . . . . . . . H6 previous H8 H9)
we proved
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
by (or_intror . . previous)
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
we proved
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
∀d1:C
.∀t:T
.∀H4:drop (S n0) O (CHead c0 (Bind Void) u1) (CHead d1 (Bind Abst) t)
.or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t
case csubt_abst : c0:C c3:C H1:csubt g c0 c3 u:T t:T :ty3 g c0 u t :ty3 g c3 u t ⇒
the thesis becomes
∀d1:C
.∀t0:T
.∀H5:drop (S n0) O (CHead c0 (Bind Abst) t) (CHead d1 (Bind Abst) t0)
.or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abst) t0)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t0
λd2:C.λu0:T.ty3 g d2 u0 t0
() by induction hypothesis we know
∀d1:C
.∀t:T
.drop (S n0) O c0 (CHead d1 (Bind Abst) t)
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O c3 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O c3 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
assume d1: C
assume t0: T
suppose H5: drop (S n0) O (CHead c0 (Bind Abst) t) (CHead d1 (Bind Abst) t0)
by (drop_gen_drop . . . . . H5)
we proved drop (r (Bind Abst) n0) O c0 (CHead d1 (Bind Abst) t0)
that is equivalent to drop n0 O c0 (CHead d1 (Bind Abst) t0)
by (H . . H1 . . previous)
we proved
or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop n0 O c3 (CHead d2 (Bind Abst) t0)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop n0 O c3 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t0
λd2:C.λu:T.ty3 g d2 u t0
we proceed by induction on the previous result to prove
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abst) t0)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t0
λd2:C.λu0:T.ty3 g d2 u0 t0
case or_introl : H6:ex2 C λd2:C.csubt g d1 d2 λd2:C.drop n0 O c3 (CHead d2 (Bind Abst) t0) ⇒
the thesis becomes
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abst) t0)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t0
λd2:C.λu0:T.ty3 g d2 u0 t0
we proceed by induction on H6 to prove
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abst) t0)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t0
λd2:C.λu0:T.ty3 g d2 u0 t0
case ex_intro2 : x:C H7:csubt g d1 x H8:drop n0 O c3 (CHead x (Bind Abst) t0) ⇒
the thesis becomes
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abst) t0)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t0
λd2:C.λu0:T.ty3 g d2 u0 t0
consider H8
we proved drop n0 O c3 (CHead x (Bind Abst) t0)
that is equivalent to drop (r (Bind Abbr) n0) O c3 (CHead x (Bind Abst) t0)
by (drop_drop . . . . previous .)
we proved drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead x (Bind Abst) t0)
by (ex_intro2 . . . . H7 previous)
we proved
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abst) t0)
by (or_introl . . previous)
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abst) t0)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t0
λd2:C.λu0:T.ty3 g d2 u0 t0
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abst) t0)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t0
λd2:C.λu0:T.ty3 g d2 u0 t0
case or_intror : H6:ex4_2 C T λd2:C.λ:T.csubt g d1 d2 λd2:C.λu0:T.drop n0 O c3 (CHead d2 (Bind Abbr) u0) λ:C.λu0:T.ty3 g d1 u0 t0 λd2:C.λu0:T.ty3 g d2 u0 t0 ⇒
the thesis becomes
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abst) t0)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t0
λd2:C.λu0:T.ty3 g d2 u0 t0
we proceed by induction on H6 to prove
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abst) t0)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t0
λd2:C.λu0:T.ty3 g d2 u0 t0
case ex4_2_intro : x0:C x1:T H7:csubt g d1 x0 H8:drop n0 O c3 (CHead x0 (Bind Abbr) x1) H9:ty3 g d1 x1 t0 H10:ty3 g x0 x1 t0 ⇒
the thesis becomes
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abst) t0)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t0
λd2:C.λu0:T.ty3 g d2 u0 t0
consider H8
we proved drop n0 O c3 (CHead x0 (Bind Abbr) x1)
that is equivalent to drop (r (Bind Abbr) n0) O c3 (CHead x0 (Bind Abbr) x1)
by (drop_drop . . . . previous .)
we proved drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead x0 (Bind Abbr) x1)
by (ex4_2_intro . . . . . . . . H7 previous H9 H10)
we proved
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t0
λd2:C.λu0:T.ty3 g d2 u0 t0
by (or_intror . . previous)
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abst) t0)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t0
λd2:C.λu0:T.ty3 g d2 u0 t0
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abst) t0)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t0
λd2:C.λu0:T.ty3 g d2 u0 t0
we proved
or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abst) t0)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t0
λd2:C.λu0:T.ty3 g d2 u0 t0
∀d1:C
.∀t0:T
.∀H5:drop (S n0) O (CHead c0 (Bind Abst) t) (CHead d1 (Bind Abst) t0)
.or
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abst) t0)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu0:T.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Bind Abbr) u0)
λ:C.λu0:T.ty3 g d1 u0 t0
λd2:C.λu0:T.ty3 g d2 u0 t0
we proved
∀d1:C
.∀t:T
.drop (S n0) O c1 (CHead d1 (Bind Abst) t)
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
∀c1:C
.∀c2:C
.∀H0:csubt g c1 c2
.∀d1:C
.∀t:T
.drop (S n0) O c1 (CHead d1 (Bind Abst) t)
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop (S n0) O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
we proved
∀c1:C
.∀c2:C
.csubt g c1 c2
→∀d1:C
.∀t:T
.drop n O c1 (CHead d1 (Bind Abst) t)
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop n O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop n O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)
we proved
∀g:G
.∀n:nat
.∀c1:C
.∀c2:C
.csubt g c1 c2
→∀d1:C
.∀t:T
.drop n O c1 (CHead d1 (Bind Abst) t)
→(or
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop n O c2 (CHead d2 (Bind Abst) t)
ex4_2
C
T
λd2:C.λ:T.csubt g d1 d2
λd2:C.λu:T.drop n O c2 (CHead d2 (Bind Abbr) u)
λ:C.λu:T.ty3 g d1 u t
λd2:C.λu:T.ty3 g d2 u t)