DEFINITION csubt_clear_conf()
TYPE =
∀g:G.∀c1:C.∀c2:C.(csubt g c1 c2)→∀e1:C.(clear c1 e1)→(ex2 C λe2:C.csubt g e1 e2 λe2:C.clear c2 e2)
BODY =
assume g: G
assume c1: C
assume c2: C
suppose H: csubt g c1 c2
we proceed by induction on H to prove ∀e1:C.(clear c1 e1)→(ex2 C λe2:C.csubt g e1 e2 λe2:C.clear c2 e2)
case csubt_sort : n:nat ⇒
the thesis becomes ∀e1:C.∀H0:(clear (CSort n) e1).(ex2 C λe2:C.csubt g e1 e2 λe2:C.clear (CSort n) e2)
assume e1: C
suppose H0: clear (CSort n) e1
by (clear_gen_sort . . H0 .)
we proved ex2 C λe2:C.csubt g e1 e2 λe2:C.clear (CSort n) e2
∀e1:C.∀H0:(clear (CSort n) e1).(ex2 C λe2:C.csubt g e1 e2 λe2:C.clear (CSort n) e2)
case csubt_head : c3:C c4:C H0:csubt g c3 c4 k:K u:T ⇒
the thesis becomes ∀e1:C.∀H2:(clear (CHead c3 k u) e1).(ex2 C λe2:C.csubt g e1 e2 λe2:C.clear (CHead c4 k u) e2)
(H1) by induction hypothesis we know ∀e1:C.(clear c3 e1)→(ex2 C λe2:C.csubt g e1 e2 λe2:C.clear c4 e2)
assume e1: C
suppose H2: clear (CHead c3 k u) e1
assume b: B
suppose H3: clear (CHead c3 (Bind b) u) e1
(h1)
(h1)
by (csubt_head . . . H0 . .)
csubt g (CHead c3 (Bind b) u) (CHead c4 (Bind b) u)
end of h1
(h2)
by (clear_bind . . .)
clear (CHead c4 (Bind b) u) (CHead c4 (Bind b) u)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
C
λe2:C.csubt g (CHead c3 (Bind b) u) e2
λe2:C.clear (CHead c4 (Bind b) u) e2
end of h1
(h2)
by (clear_gen_bind . . . . H3)
eq C e1 (CHead c3 (Bind b) u)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved ex2 C λe2:C.csubt g e1 e2 λe2:C.clear (CHead c4 (Bind b) u) e2
∀H3:clear (CHead c3 (Bind b) u) e1
.ex2 C λe2:C.csubt g e1 e2 λe2:C.clear (CHead c4 (Bind b) u) e2
assume f: F
suppose H3: clear (CHead c3 (Flat f) u) e1
(H4)
by (clear_gen_flat . . . . H3)
we proved clear c3 e1
by (H1 . previous)
ex2 C λe2:C.csubt g e1 e2 λe2:C.clear c4 e2
end of H4
we proceed by induction on H4 to prove ex2 C λe2:C.csubt g e1 e2 λe2:C.clear (CHead c4 (Flat f) u) e2
case ex_intro2 : x:C H5:csubt g e1 x H6:clear c4 x ⇒
the thesis becomes ex2 C λe2:C.csubt g e1 e2 λe2:C.clear (CHead c4 (Flat f) u) e2
by (clear_flat . . H6 . .)
we proved clear (CHead c4 (Flat f) u) x
by (ex_intro2 . . . . H5 previous)
ex2 C λe2:C.csubt g e1 e2 λe2:C.clear (CHead c4 (Flat f) u) e2
we proved ex2 C λe2:C.csubt g e1 e2 λe2:C.clear (CHead c4 (Flat f) u) e2
∀H3:clear (CHead c3 (Flat f) u) e1
.ex2 C λe2:C.csubt g e1 e2 λe2:C.clear (CHead c4 (Flat f) u) e2
by (previous . H2)
we proved ex2 C λe2:C.csubt g e1 e2 λe2:C.clear (CHead c4 k u) e2
∀e1:C.∀H2:(clear (CHead c3 k u) e1).(ex2 C λe2:C.csubt g e1 e2 λe2:C.clear (CHead c4 k u) e2)
case csubt_void : c3:C c4:C H0:csubt g c3 c4 b:B H2:not (eq B b Void) u1:T u2:T ⇒
the thesis becomes
∀e1:C
.∀H3:clear (CHead c3 (Bind Void) u1) e1
.ex2 C λe2:C.csubt g e1 e2 λe2:C.clear (CHead c4 (Bind b) u2) e2
() by induction hypothesis we know ∀e1:C.(clear c3 e1)→(ex2 C λe2:C.csubt g e1 e2 λe2:C.clear c4 e2)
assume e1: C
suppose H3: clear (CHead c3 (Bind Void) u1) e1
(h1)
(h1)
by (csubt_void . . . H0 . H2 . .)
csubt g (CHead c3 (Bind Void) u1) (CHead c4 (Bind b) u2)
end of h1
(h2)
by (clear_bind . . .)
clear (CHead c4 (Bind b) u2) (CHead c4 (Bind b) u2)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
C
λe2:C.csubt g (CHead c3 (Bind Void) u1) e2
λe2:C.clear (CHead c4 (Bind b) u2) e2
end of h1
(h2)
by (clear_gen_bind . . . . H3)
eq C e1 (CHead c3 (Bind Void) u1)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved ex2 C λe2:C.csubt g e1 e2 λe2:C.clear (CHead c4 (Bind b) u2) e2
∀e1:C
.∀H3:clear (CHead c3 (Bind Void) u1) e1
.ex2 C λe2:C.csubt g e1 e2 λe2:C.clear (CHead c4 (Bind b) u2) e2
case csubt_abst : c3:C c4:C H0:csubt g c3 c4 u:T t:T H2:ty3 g c3 u t H3:ty3 g c4 u t ⇒
the thesis becomes
∀e1:C
.∀H4:clear (CHead c3 (Bind Abst) t) e1
.ex2 C λe2:C.csubt g e1 e2 λe2:C.clear (CHead c4 (Bind Abbr) u) e2
() by induction hypothesis we know ∀e1:C.(clear c3 e1)→(ex2 C λe2:C.csubt g e1 e2 λe2:C.clear c4 e2)
assume e1: C
suppose H4: clear (CHead c3 (Bind Abst) t) e1
(h1)
(h1)
by (csubt_abst . . . H0 . . H2 H3)
csubt g (CHead c3 (Bind Abst) t) (CHead c4 (Bind Abbr) u)
end of h1
(h2)
by (clear_bind . . .)
clear (CHead c4 (Bind Abbr) u) (CHead c4 (Bind Abbr) u)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
C
λe2:C.csubt g (CHead c3 (Bind Abst) t) e2
λe2:C.clear (CHead c4 (Bind Abbr) u) e2
end of h1
(h2)
by (clear_gen_bind . . . . H4)
eq C e1 (CHead c3 (Bind Abst) t)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved ex2 C λe2:C.csubt g e1 e2 λe2:C.clear (CHead c4 (Bind Abbr) u) e2
∀e1:C
.∀H4:clear (CHead c3 (Bind Abst) t) e1
.ex2 C λe2:C.csubt g e1 e2 λe2:C.clear (CHead c4 (Bind Abbr) u) e2
we proved ∀e1:C.(clear c1 e1)→(ex2 C λe2:C.csubt g e1 e2 λe2:C.clear c2 e2)
we proved
∀g:G.∀c1:C.∀c2:C.(csubt g c1 c2)→∀e1:C.(clear c1 e1)→(ex2 C λe2:C.csubt g e1 e2 λe2:C.clear c2 e2)