DEFINITION csubt_drop_flat()
TYPE =
∀g:G
.∀f:F
.∀n:nat
.∀c1:C
.∀c2:C
.csubt g c1 c2
→∀d1:C
.∀u:T
.drop n O c1 (CHead d1 (Flat f) u)
→ex2 C λd2:C.csubt g d1 d2 λd2:C.drop n O c2 (CHead d2 (Flat f) u)
BODY =
assume g: G
assume f: F
assume n: nat
we proceed by induction on n to prove
∀c1:C
.∀c2:C
.csubt g c1 c2
→∀d1:C
.∀u:T
.drop n O c1 (CHead d1 (Flat f) u)
→ex2 C λd2:C.csubt g d1 d2 λd2:C.drop n O c2 (CHead d2 (Flat f) u)
case O : ⇒
the thesis becomes
∀c1:C
.∀c2:C
.csubt g c1 c2
→∀d1:C
.∀u:T
.drop O O c1 (CHead d1 (Flat f) u)
→ex2 C λd2:C.csubt g d1 d2 λd2:C.drop O O c2 (CHead d2 (Flat f) u)
assume c1: C
assume c2: C
suppose H: csubt g c1 c2
assume d1: C
assume u: T
suppose H0: drop O O c1 (CHead d1 (Flat f) u)
(H1)
by (drop_gen_refl . . H0)
we proved eq C c1 (CHead d1 (Flat f) u)
we proceed by induction on the previous result to prove csubt g (CHead d1 (Flat f) u) c2
case refl_equal : ⇒
the thesis becomes the hypothesis H
csubt g (CHead d1 (Flat f) u) c2
end of H1
(H_x)
by (csubt_gen_flat . . . . . H1)
ex2 C λe2:C.eq C c2 (CHead e2 (Flat f) u) λe2:C.csubt g d1 e2
end of H_x
(H2) consider H_x
we proceed by induction on H2 to prove ex2 C λd2:C.csubt g d1 d2 λd2:C.drop O O c2 (CHead d2 (Flat f) u)
case ex_intro2 : x:C H3:eq C c2 (CHead x (Flat f) u) H4:csubt g d1 x ⇒
the thesis becomes ex2 C λd2:C.csubt g d1 d2 λd2:C.drop O O c2 (CHead d2 (Flat f) u)
by (drop_refl .)
we proved drop O O (CHead x (Flat f) u) (CHead x (Flat f) u)
by (ex_intro2 . . . . H4 previous)
we proved
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop O O (CHead x (Flat f) u) (CHead d2 (Flat f) u)
by (eq_ind_r . . . previous . H3)
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop O O c2 (CHead d2 (Flat f) u)
we proved ex2 C λd2:C.csubt g d1 d2 λd2:C.drop O O c2 (CHead d2 (Flat f) u)
∀c1:C
.∀c2:C
.csubt g c1 c2
→∀d1:C
.∀u:T
.drop O O c1 (CHead d1 (Flat f) u)
→ex2 C λd2:C.csubt g d1 d2 λd2:C.drop O O c2 (CHead d2 (Flat f) u)
case S : n0:nat ⇒
the thesis becomes
∀c1:C
.∀c2:C
.∀H0:csubt g c1 c2
.∀d1:C
.∀u:T
.drop (S n0) O c1 (CHead d1 (Flat f) u)
→ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O c2 (CHead d2 (Flat f) u)
(H) by induction hypothesis we know
∀c1:C
.∀c2:C
.csubt g c1 c2
→∀d1:C
.∀u:T
.drop n0 O c1 (CHead d1 (Flat f) u)
→ex2 C λd2:C.csubt g d1 d2 λd2:C.drop n0 O c2 (CHead d2 (Flat f) u)
assume c1: C
assume c2: C
suppose H0: csubt g c1 c2
we proceed by induction on H0 to prove
∀d1:C
.∀u:T
.drop (S n0) O c1 (CHead d1 (Flat f) u)
→ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O c2 (CHead d2 (Flat f) u)
case csubt_sort : n1:nat ⇒
the thesis becomes
∀d1:C
.∀u:T
.∀H1:drop (S n0) O (CSort n1) (CHead d1 (Flat f) u)
.ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O (CSort n1) (CHead d2 (Flat f) u)
assume d1: C
assume u: T
suppose H1: drop (S n0) O (CSort n1) (CHead d1 (Flat f) u)
by (drop_gen_sort . . . . H1)
we proved
and3
eq C (CHead d1 (Flat f) u) (CSort n1)
eq nat (S n0) O
eq nat O O
we proceed by induction on the previous result to prove ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O (CSort n1) (CHead d2 (Flat f) u)
case and3_intro : :eq C (CHead d1 (Flat f) u) (CSort n1) H3:eq nat (S n0) O :eq nat O O ⇒
the thesis becomes ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O (CSort n1) (CHead d2 (Flat f) u)
(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 ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O (CSort n1) (CHead d2 (Flat f) u)
ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O (CSort n1) (CHead d2 (Flat f) u)
we proved ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O (CSort n1) (CHead d2 (Flat f) u)
∀d1:C
.∀u:T
.∀H1:drop (S n0) O (CSort n1) (CHead d1 (Flat f) u)
.ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O (CSort n1) (CHead d2 (Flat f) u)
case csubt_head ⇒
we need to prove
∀c0:C
.∀c3:C
.csubt g c0 c3
→(∀d1:C
.∀u:T
.drop (S n0) O c0 (CHead d1 (Flat f) u)
→ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O c3 (CHead d2 (Flat f) u)
→∀k:K
.∀u:T
.∀d1:C
.∀u0:T
.drop (S n0) O (CHead c0 k u) (CHead d1 (Flat f) u0)
→ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O (CHead c3 k u) (CHead d2 (Flat f) u0))
assume c0: C
assume c3: C
suppose H1: csubt g c0 c3
suppose H2:
∀d1:C
.∀u:T
.drop (S n0) O c0 (CHead d1 (Flat f) u)
→ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O c3 (CHead d2 (Flat f) u)
assume k: K
we proceed by induction on k to prove
∀u:T
.∀d1:C
.∀u0:T
.drop (S n0) O (CHead c0 k u) (CHead d1 (Flat f) u0)
→ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O (CHead c3 k u) (CHead d2 (Flat f) u0)
case Bind : b:B ⇒
the thesis becomes
∀u:T
.∀d1:C
.∀u0:T
.∀H3:drop (S n0) O (CHead c0 (Bind b) u) (CHead d1 (Flat f) u0)
.ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Flat f) u0)
assume u: T
assume d1: C
assume u0: T
suppose H3: drop (S n0) O (CHead c0 (Bind b) u) (CHead d1 (Flat f) u0)
by (drop_gen_drop . . . . . H3)
we proved drop (r (Bind b) n0) O c0 (CHead d1 (Flat f) u0)
that is equivalent to drop n0 O c0 (CHead d1 (Flat f) u0)
by (H . . H1 . . previous)
we proved ex2 C λd2:C.csubt g d1 d2 λd2:C.drop n0 O c3 (CHead d2 (Flat f) u0)
we proceed by induction on the previous result to prove
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Flat f) u0)
case ex_intro2 : x:C H4:csubt g d1 x H5:drop n0 O c3 (CHead x (Flat f) u0) ⇒
the thesis becomes
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Flat f) u0)
consider H5
we proved drop n0 O c3 (CHead x (Flat f) u0)
that is equivalent to drop (r (Bind b) n0) O c3 (CHead x (Flat f) u0)
by (drop_drop . . . . previous .)
we proved drop (S n0) O (CHead c3 (Bind b) u) (CHead x (Flat f) u0)
by (ex_intro2 . . . . H4 previous)
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Flat f) u0)
we proved
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Flat f) u0)
∀u:T
.∀d1:C
.∀u0:T
.∀H3:drop (S n0) O (CHead c0 (Bind b) u) (CHead d1 (Flat f) u0)
.ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u) (CHead d2 (Flat f) u0)
case Flat : f0:F ⇒
the thesis becomes
∀u:T
.∀d1:C
.∀u0:T
.∀H3:drop (S n0) O (CHead c0 (Flat f0) u) (CHead d1 (Flat f) u0)
.ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Flat f0) u) (CHead d2 (Flat f) u0)
assume u: T
assume d1: C
assume u0: T
suppose H3: drop (S n0) O (CHead c0 (Flat f0) u) (CHead d1 (Flat f) u0)
by (drop_gen_drop . . . . . H3)
we proved drop (r (Flat f0) n0) O c0 (CHead d1 (Flat f) u0)
that is equivalent to drop (S n0) O c0 (CHead d1 (Flat f) u0)
by (H2 . . previous)
we proved ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O c3 (CHead d2 (Flat f) u0)
we proceed by induction on the previous result to prove
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Flat f0) u) (CHead d2 (Flat f) u0)
case ex_intro2 : x:C H4:csubt g d1 x H5:drop (S n0) O c3 (CHead x (Flat f) u0) ⇒
the thesis becomes
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Flat f0) u) (CHead d2 (Flat f) u0)
consider H5
we proved drop (S n0) O c3 (CHead x (Flat f) u0)
that is equivalent to drop (r (Flat f0) n0) O c3 (CHead x (Flat f) u0)
by (drop_drop . . . . previous .)
we proved drop (S n0) O (CHead c3 (Flat f0) u) (CHead x (Flat f) u0)
by (ex_intro2 . . . . H4 previous)
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Flat f0) u) (CHead d2 (Flat f) u0)
we proved
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Flat f0) u) (CHead d2 (Flat f) u0)
∀u:T
.∀d1:C
.∀u0:T
.∀H3:drop (S n0) O (CHead c0 (Flat f0) u) (CHead d1 (Flat f) u0)
.ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Flat f0) u) (CHead d2 (Flat f) u0)
we proved
∀u:T
.∀d1:C
.∀u0:T
.drop (S n0) O (CHead c0 k u) (CHead d1 (Flat f) u0)
→ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O (CHead c3 k u) (CHead d2 (Flat f) u0)
∀c0:C
.∀c3:C
.csubt g c0 c3
→(∀d1:C
.∀u:T
.drop (S n0) O c0 (CHead d1 (Flat f) u)
→ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O c3 (CHead d2 (Flat f) u)
→∀k:K
.∀u:T
.∀d1:C
.∀u0:T
.drop (S n0) O (CHead c0 k u) (CHead d1 (Flat f) u0)
→ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O (CHead c3 k u) (CHead d2 (Flat f) u0))
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
.∀u:T
.∀H4:drop (S n0) O (CHead c0 (Bind Void) u1) (CHead d1 (Flat f) u)
.ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Flat f) u)
() by induction hypothesis we know
∀d1:C
.∀u:T
.drop (S n0) O c0 (CHead d1 (Flat f) u)
→ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O c3 (CHead d2 (Flat f) u)
assume d1: C
assume u: T
suppose H4: drop (S n0) O (CHead c0 (Bind Void) u1) (CHead d1 (Flat f) u)
by (drop_gen_drop . . . . . H4)
we proved drop (r (Bind Void) n0) O c0 (CHead d1 (Flat f) u)
that is equivalent to drop n0 O c0 (CHead d1 (Flat f) u)
by (H . . H1 . . previous)
we proved ex2 C λd2:C.csubt g d1 d2 λd2:C.drop n0 O c3 (CHead d2 (Flat f) u)
we proceed by induction on the previous result to prove
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Flat f) u)
case ex_intro2 : x:C H5:csubt g d1 x H6:drop n0 O c3 (CHead x (Flat f) u) ⇒
the thesis becomes
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Flat f) u)
consider H6
we proved drop n0 O c3 (CHead x (Flat f) u)
that is equivalent to drop (r (Bind b) n0) O c3 (CHead x (Flat f) u)
by (drop_drop . . . . previous .)
we proved drop (S n0) O (CHead c3 (Bind b) u2) (CHead x (Flat f) u)
by (ex_intro2 . . . . H5 previous)
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Flat f) u)
we proved
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Flat f) u)
∀d1:C
.∀u:T
.∀H4:drop (S n0) O (CHead c0 (Bind Void) u1) (CHead d1 (Flat f) u)
.ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind b) u2) (CHead d2 (Flat f) u)
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
.∀u0:T
.∀H5:drop (S n0) O (CHead c0 (Bind Abst) t) (CHead d1 (Flat f) u0)
.ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Flat f) u0)
() by induction hypothesis we know
∀d1:C
.∀u:T
.drop (S n0) O c0 (CHead d1 (Flat f) u)
→ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O c3 (CHead d2 (Flat f) u)
assume d1: C
assume u0: T
suppose H5: drop (S n0) O (CHead c0 (Bind Abst) t) (CHead d1 (Flat f) u0)
by (drop_gen_drop . . . . . H5)
we proved drop (r (Bind Abst) n0) O c0 (CHead d1 (Flat f) u0)
that is equivalent to drop n0 O c0 (CHead d1 (Flat f) u0)
by (H . . H1 . . previous)
we proved ex2 C λd2:C.csubt g d1 d2 λd2:C.drop n0 O c3 (CHead d2 (Flat f) u0)
we proceed by induction on the previous result to prove
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Flat f) u0)
case ex_intro2 : x:C H6:csubt g d1 x H7:drop n0 O c3 (CHead x (Flat f) u0) ⇒
the thesis becomes
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Flat f) u0)
consider H7
we proved drop n0 O c3 (CHead x (Flat f) u0)
that is equivalent to drop (r (Bind Abbr) n0) O c3 (CHead x (Flat f) u0)
by (drop_drop . . . . previous .)
we proved drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead x (Flat f) u0)
by (ex_intro2 . . . . H6 previous)
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Flat f) u0)
we proved
ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Flat f) u0)
∀d1:C
.∀u0:T
.∀H5:drop (S n0) O (CHead c0 (Bind Abst) t) (CHead d1 (Flat f) u0)
.ex2
C
λd2:C.csubt g d1 d2
λd2:C.drop (S n0) O (CHead c3 (Bind Abbr) u) (CHead d2 (Flat f) u0)
we proved
∀d1:C
.∀u:T
.drop (S n0) O c1 (CHead d1 (Flat f) u)
→ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O c2 (CHead d2 (Flat f) u)
∀c1:C
.∀c2:C
.∀H0:csubt g c1 c2
.∀d1:C
.∀u:T
.drop (S n0) O c1 (CHead d1 (Flat f) u)
→ex2 C λd2:C.csubt g d1 d2 λd2:C.drop (S n0) O c2 (CHead d2 (Flat f) u)
we proved
∀c1:C
.∀c2:C
.csubt g c1 c2
→∀d1:C
.∀u:T
.drop n O c1 (CHead d1 (Flat f) u)
→ex2 C λd2:C.csubt g d1 d2 λd2:C.drop n O c2 (CHead d2 (Flat f) u)
we proved
∀g:G
.∀f:F
.∀n:nat
.∀c1:C
.∀c2:C
.csubt g c1 c2
→∀d1:C
.∀u:T
.drop n O c1 (CHead d1 (Flat f) u)
→ex2 C λd2:C.csubt g d1 d2 λd2:C.drop n O c2 (CHead d2 (Flat f) u)