DEFINITION csuba_clear_trans()
TYPE =
∀g:G.∀c1:C.∀c2:C.(csuba g c2 c1)→∀e1:C.(clear c1 e1)→(ex2 C λe2:C.csuba g e2 e1 λe2:C.clear c2 e2)
BODY =
assume g: G
assume c1: C
assume c2: C
suppose H: csuba g c2 c1
we proceed by induction on H to prove ∀e1:C.(clear c1 e1)→(ex2 C λe2:C.csuba g e2 e1 λe2:C.clear c2 e2)
case csuba_sort : n:nat ⇒
the thesis becomes ∀e1:C.∀H0:(clear (CSort n) e1).(ex2 C λe2:C.csuba g e2 e1 λ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.csuba g e2 e1 λe2:C.clear (CSort n) e2
∀e1:C.∀H0:(clear (CSort n) e1).(ex2 C λe2:C.csuba g e2 e1 λe2:C.clear (CSort n) e2)
case csuba_head : c3:C c4:C H0:csuba g c3 c4 k:K u:T ⇒
the thesis becomes ∀e1:C.∀H2:(clear (CHead c4 k u) e1).(ex2 C λe2:C.csuba g e2 e1 λe2:C.clear (CHead c3 k u) e2)
(H1) by induction hypothesis we know ∀e1:C.(clear c4 e1)→(ex2 C λe2:C.csuba g e2 e1 λe2:C.clear c3 e2)
assume e1: C
suppose H2: clear (CHead c4 k u) e1
assume b: B
suppose H3: clear (CHead c4 (Bind b) u) e1
(h1)
(h1)
by (csuba_head . . . H0 . .)
csuba g (CHead c3 (Bind b) u) (CHead c4 (Bind b) u)
end of h1
(h2)
by (clear_bind . . .)
clear (CHead c3 (Bind b) u) (CHead c3 (Bind b) u)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
C
λe2:C.csuba g e2 (CHead c4 (Bind b) u)
λe2:C.clear (CHead c3 (Bind b) u) e2
end of h1
(h2)
by (clear_gen_bind . . . . H3)
eq C e1 (CHead c4 (Bind b) u)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved ex2 C λe2:C.csuba g e2 e1 λe2:C.clear (CHead c3 (Bind b) u) e2
∀H3:clear (CHead c4 (Bind b) u) e1
.ex2 C λe2:C.csuba g e2 e1 λe2:C.clear (CHead c3 (Bind b) u) e2
assume f: F
suppose H3: clear (CHead c4 (Flat f) u) e1
(H4)
by (clear_gen_flat . . . . H3)
we proved clear c4 e1
by (H1 . previous)
ex2 C λe2:C.csuba g e2 e1 λe2:C.clear c3 e2
end of H4
we proceed by induction on H4 to prove ex2 C λe2:C.csuba g e2 e1 λe2:C.clear (CHead c3 (Flat f) u) e2
case ex_intro2 : x:C H5:csuba g x e1 H6:clear c3 x ⇒
the thesis becomes ex2 C λe2:C.csuba g e2 e1 λe2:C.clear (CHead c3 (Flat f) u) e2
by (clear_flat . . H6 . .)
we proved clear (CHead c3 (Flat f) u) x
by (ex_intro2 . . . . H5 previous)
ex2 C λe2:C.csuba g e2 e1 λe2:C.clear (CHead c3 (Flat f) u) e2
we proved ex2 C λe2:C.csuba g e2 e1 λe2:C.clear (CHead c3 (Flat f) u) e2
∀H3:clear (CHead c4 (Flat f) u) e1
.ex2 C λe2:C.csuba g e2 e1 λe2:C.clear (CHead c3 (Flat f) u) e2
by (previous . H2)
we proved ex2 C λe2:C.csuba g e2 e1 λe2:C.clear (CHead c3 k u) e2
∀e1:C.∀H2:(clear (CHead c4 k u) e1).(ex2 C λe2:C.csuba g e2 e1 λe2:C.clear (CHead c3 k u) e2)
case csuba_void : c3:C c4:C H0:csuba g c3 c4 b:B H2:not (eq B b Void) u1:T u2:T ⇒
the thesis becomes
∀e1:C
.∀H3:clear (CHead c4 (Bind b) u2) e1
.ex2 C λe2:C.csuba g e2 e1 λe2:C.clear (CHead c3 (Bind Void) u1) e2
() by induction hypothesis we know ∀e1:C.(clear c4 e1)→(ex2 C λe2:C.csuba g e2 e1 λe2:C.clear c3 e2)
assume e1: C
suppose H3: clear (CHead c4 (Bind b) u2) e1
(h1)
(h1)
by (csuba_void . . . H0 . H2 . .)
csuba g (CHead c3 (Bind Void) u1) (CHead c4 (Bind b) u2)
end of h1
(h2)
by (clear_bind . . .)
clear (CHead c3 (Bind Void) u1) (CHead c3 (Bind Void) u1)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
C
λe2:C.csuba g e2 (CHead c4 (Bind b) u2)
λe2:C.clear (CHead c3 (Bind Void) u1) e2
end of h1
(h2)
by (clear_gen_bind . . . . H3)
eq C e1 (CHead c4 (Bind b) u2)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved ex2 C λe2:C.csuba g e2 e1 λe2:C.clear (CHead c3 (Bind Void) u1) e2
∀e1:C
.∀H3:clear (CHead c4 (Bind b) u2) e1
.ex2 C λe2:C.csuba g e2 e1 λe2:C.clear (CHead c3 (Bind Void) u1) e2
case csuba_abst : c3:C c4:C H0:csuba g c3 c4 t:T a:A H2:arity g c3 t (asucc g a) u:T H3:arity g c4 u a ⇒
the thesis becomes
∀e1:C
.∀H4:clear (CHead c4 (Bind Abbr) u) e1
.ex2 C λe2:C.csuba g e2 e1 λe2:C.clear (CHead c3 (Bind Abst) t) e2
() by induction hypothesis we know ∀e1:C.(clear c4 e1)→(ex2 C λe2:C.csuba g e2 e1 λe2:C.clear c3 e2)
assume e1: C
suppose H4: clear (CHead c4 (Bind Abbr) u) e1
(h1)
(h1)
by (csuba_abst . . . H0 . . H2 . H3)
csuba g (CHead c3 (Bind Abst) t) (CHead c4 (Bind Abbr) u)
end of h1
(h2)
by (clear_bind . . .)
clear (CHead c3 (Bind Abst) t) (CHead c3 (Bind Abst) t)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
C
λe2:C.csuba g e2 (CHead c4 (Bind Abbr) u)
λe2:C.clear (CHead c3 (Bind Abst) t) e2
end of h1
(h2)
by (clear_gen_bind . . . . H4)
eq C e1 (CHead c4 (Bind Abbr) u)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved ex2 C λe2:C.csuba g e2 e1 λe2:C.clear (CHead c3 (Bind Abst) t) e2
∀e1:C
.∀H4:clear (CHead c4 (Bind Abbr) u) e1
.ex2 C λe2:C.csuba g e2 e1 λe2:C.clear (CHead c3 (Bind Abst) t) e2
we proved ∀e1:C.(clear c1 e1)→(ex2 C λe2:C.csuba g e2 e1 λe2:C.clear c2 e2)
we proved
∀g:G.∀c1:C.∀c2:C.(csuba g c2 c1)→∀e1:C.(clear c1 e1)→(ex2 C λe2:C.csuba g e2 e1 λe2:C.clear c2 e2)