DEFINITION getl_clear_conf()
TYPE =
∀i:nat.∀c1:C.∀c3:C.(getl i c1 c3)→∀c2:C.(clear c1 c2)→(getl i c2 c3)
BODY =
assume i: nat
we proceed by induction on i to prove ∀c1:C.∀c3:C.(getl i c1 c3)→∀c2:C.(clear c1 c2)→(getl i c2 c3)
case O : ⇒
the thesis becomes ∀c1:C.∀c3:C.(getl O c1 c3)→∀c2:C.(clear c1 c2)→(getl O c2 c3)
assume c1: C
assume c3: C
suppose H: getl O c1 c3
assume c2: C
suppose H0: clear c1 c2
by (getl_gen_O . . H)
we proved clear c1 c3
by (clear_mono . . previous . H0)
we proved eq C c3 c2
we proceed by induction on the previous result to prove getl O c2 c3
case refl_equal : ⇒
the thesis becomes getl O c3 c3
(H1)
by (getl_gen_O . . H)
we proved clear c1 c3
by (clear_gen_all . . previous)
ex_3 B C T λb:B.λe:C.λu:T.eq C c3 (CHead e (Bind b) u)
end of H1
we proceed by induction on H1 to prove getl O c3 c3
case ex_3_intro : x0:B x1:C x2:T H2:eq C c3 (CHead x1 (Bind x0) x2) ⇒
the thesis becomes getl O c3 c3
by (getl_refl . . .)
we proved getl O (CHead x1 (Bind x0) x2) (CHead x1 (Bind x0) x2)
by (eq_ind_r . . . previous . H2)
getl O c3 c3
getl O c3 c3
we proved getl O c2 c3
∀c1:C.∀c3:C.(getl O c1 c3)→∀c2:C.(clear c1 c2)→(getl O c2 c3)
case S : n:nat ⇒
the thesis becomes ∀c1:C.∀c3:C.(getl (S n) c1 c3)→∀c2:C.(clear c1 c2)→(getl (S n) c2 c3)
() by induction hypothesis we know ∀c1:C.∀c3:C.(getl n c1 c3)→∀c2:C.(clear c1 c2)→(getl n c2 c3)
assume c1: C
we proceed by induction on c1 to prove ∀c3:C.(getl (S n) c1 c3)→∀c2:C.(clear c1 c2)→(getl (S n) c2 c3)
case CSort : n0:nat ⇒
the thesis becomes
∀c3:C.∀H0:(getl (S n) (CSort n0) c3).∀c2:C.(clear (CSort n0) c2)→(getl (S n) c2 c3)
assume c3: C
suppose H0: getl (S n) (CSort n0) c3
assume c2: C
suppose : clear (CSort n0) c2
by (getl_gen_sort . . . H0 .)
we proved getl (S n) c2 c3
∀c3:C.∀H0:(getl (S n) (CSort n0) c3).∀c2:C.(clear (CSort n0) c2)→(getl (S n) c2 c3)
case CHead : c:C k:K t:T ⇒
the thesis becomes
∀c3:C
.∀H1:(getl (S n) (CHead c k t) c3).∀c2:C.∀H2:(clear (CHead c k t) c2).(getl (S n) c2 c3)
(H0) by induction hypothesis we know ∀c3:C.(getl (S n) c c3)→∀c2:C.(clear c c2)→(getl (S n) c2 c3)
assume c3: C
suppose H1: getl (S n) (CHead c k t) c3
assume c2: C
suppose H2: clear (CHead c k t) c2
assume b: B
suppose H3: getl (S n) (CHead c (Bind b) t) c3
suppose H4: clear (CHead c (Bind b) t) c2
(h1)
by (getl_gen_S . . . . . H3)
we proved getl (r (Bind b) n) c c3
by (getl_head . . . . previous .)
getl (S n) (CHead c (Bind b) t) c3
end of h1
(h2)
by (clear_gen_bind . . . . H4)
eq C c2 (CHead c (Bind b) t)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved getl (S n) c2 c3
∀H3:getl (S n) (CHead c (Bind b) t) c3
.∀H4:(clear (CHead c (Bind b) t) c2).(getl (S n) c2 c3)
assume f: F
suppose H3: getl (S n) (CHead c (Flat f) t) c3
suppose H4: clear (CHead c (Flat f) t) c2
(h1)
by (getl_gen_S . . . . . H3)
we proved getl (r (Flat f) n) c c3
getl (S n) c c3
end of h1
(h2)
by (clear_gen_flat . . . . H4)
clear c c2
end of h2
by (H0 . h1 . h2)
we proved getl (S n) c2 c3
∀H3:getl (S n) (CHead c (Flat f) t) c3
.∀H4:(clear (CHead c (Flat f) t) c2).(getl (S n) c2 c3)
by (previous . H1 H2)
we proved getl (S n) c2 c3
∀c3:C
.∀H1:(getl (S n) (CHead c k t) c3).∀c2:C.∀H2:(clear (CHead c k t) c2).(getl (S n) c2 c3)
we proved ∀c3:C.(getl (S n) c1 c3)→∀c2:C.(clear c1 c2)→(getl (S n) c2 c3)
∀c1:C.∀c3:C.(getl (S n) c1 c3)→∀c2:C.(clear c1 c2)→(getl (S n) c2 c3)
we proved ∀c1:C.∀c3:C.(getl i c1 c3)→∀c2:C.(clear c1 c2)→(getl i c2 c3)
we proved ∀i:nat.∀c1:C.∀c3:C.(getl i c1 c3)→∀c2:C.(clear c1 c2)→(getl i c2 c3)