DEFINITION csubst0_clear_O()
TYPE =
∀c1:C.∀c2:C.∀v:T.(csubst0 O v c1 c2)→∀c:C.(clear c1 c)→(clear c2 c)
BODY =
assume c1: C
we proceed by induction on c1 to prove ∀c2:C.∀v:T.(csubst0 O v c1 c2)→∀c0:C.(clear c1 c0)→(clear c2 c0)
case CSort : n:nat ⇒
the thesis becomes ∀c2:C.∀v:T.∀H:(csubst0 O v (CSort n) c2).∀c:C.(clear (CSort n) c)→(clear c2 c)
assume c2: C
assume v: T
suppose H: csubst0 O v (CSort n) c2
assume c: C
suppose : clear (CSort n) c
by (csubst0_gen_sort . . . . H .)
we proved clear c2 c
∀c2:C.∀v:T.∀H:(csubst0 O v (CSort n) c2).∀c:C.(clear (CSort n) c)→(clear c2 c)
case CHead : c:C k:K t:T ⇒
the thesis becomes ∀c2:C.∀v:T.∀H0:(csubst0 O v (CHead c k t) c2).∀c0:C.∀H1:(clear (CHead c k t) c0).(clear c2 c0)
(H) by induction hypothesis we know ∀c2:C.∀v:T.(csubst0 O v c c2)→∀c0:C.(clear c c0)→(clear c2 c0)
assume c2: C
assume v: T
suppose H0: csubst0 O v (CHead c k t) c2
assume c0: C
suppose H1: clear (CHead c k t) c0
by (csubst0_gen_head . . . . . . H0)
we proved
or3
ex3_2
T
nat
λ:T.λj:nat.eq nat O (s k j)
λu2:T.λ:nat.eq C c2 (CHead c k u2)
λu2:T.λj:nat.subst0 j v t u2
ex3_2
C
nat
λ:C.λj:nat.eq nat O (s k j)
λc2:C.λ:nat.eq C c2 (CHead c2 k t)
λc2:C.λj:nat.csubst0 j v c c2
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat O (s k j)
λu2:T.λc2:C.λ:nat.eq C c2 (CHead c2 k u2)
λu2:T.λ:C.λj:nat.subst0 j v t u2
λ:T.λc2:C.λj:nat.csubst0 j v c c2
we proceed by induction on the previous result to prove clear c2 c0
case or3_intro0 : H2:ex3_2 T nat λ:T.λj:nat.eq nat O (s k j) λu2:T.λ:nat.eq C c2 (CHead c k u2) λu2:T.λj:nat.subst0 j v t u2 ⇒
the thesis becomes clear c2 c0
we proceed by induction on H2 to prove clear c2 c0
case ex3_2_intro : x0:T x1:nat H3:eq nat O (s k x1) H4:eq C c2 (CHead c k x0) H5:subst0 x1 v t x0 ⇒
the thesis becomes clear c2 c0
assume b: B
suppose : clear (CHead c (Bind b) t) c0
suppose H7: eq nat O (s (Bind b) x1)
(H8)
consider H7
we proved eq nat O (s (Bind b) x1)
that is equivalent to eq nat O (S x1)
we proceed by induction on the previous result to prove <λ:nat.Prop> CASE S x1 OF O⇒True | S ⇒False
case refl_equal : ⇒
the thesis becomes <λ:nat.Prop> CASE O OF O⇒True | S ⇒False
consider I
we proved True
<λ:nat.Prop> CASE O OF O⇒True | S ⇒False
<λ:nat.Prop> CASE S x1 OF O⇒True | S ⇒False
end of H8
consider H8
we proved <λ:nat.Prop> CASE S x1 OF O⇒True | S ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove clear (CHead c (Bind b) x0) c0
we proved clear (CHead c (Bind b) x0) c0
clear (CHead c (Bind b) t) c0
→∀H7:(eq nat O (s (Bind b) x1)).(clear (CHead c (Bind b) x0) c0)
assume f: F
suppose H6: clear (CHead c (Flat f) t) c0
suppose H7: eq nat O (s (Flat f) x1)
by (clear_gen_flat . . . . H6)
we proved clear c c0
by (clear_flat . . previous . .)
we proved clear (CHead c (Flat f) x0) c0
∀H6:clear (CHead c (Flat f) t) c0
.∀H7:(eq nat O (s (Flat f) x1)).(clear (CHead c (Flat f) x0) c0)
by (previous . H1 H3)
we proved clear (CHead c k x0) c0
by (eq_ind_r . . . previous . H4)
clear c2 c0
clear c2 c0
case or3_intro1 : H2:ex3_2 C nat λ:C.λj:nat.eq nat O (s k j) λc3:C.λ:nat.eq C c2 (CHead c3 k t) λc3:C.λj:nat.csubst0 j v c c3 ⇒
the thesis becomes clear c2 c0
we proceed by induction on H2 to prove clear c2 c0
case ex3_2_intro : x0:C x1:nat H3:eq nat O (s k x1) H4:eq C c2 (CHead x0 k t) H5:csubst0 x1 v c x0 ⇒
the thesis becomes clear c2 c0
assume b: B
suppose : clear (CHead c (Bind b) t) c0
suppose H7: eq nat O (s (Bind b) x1)
(H8)
consider H7
we proved eq nat O (s (Bind b) x1)
that is equivalent to eq nat O (S x1)
we proceed by induction on the previous result to prove <λ:nat.Prop> CASE S x1 OF O⇒True | S ⇒False
case refl_equal : ⇒
the thesis becomes <λ:nat.Prop> CASE O OF O⇒True | S ⇒False
consider I
we proved True
<λ:nat.Prop> CASE O OF O⇒True | S ⇒False
<λ:nat.Prop> CASE S x1 OF O⇒True | S ⇒False
end of H8
consider H8
we proved <λ:nat.Prop> CASE S x1 OF O⇒True | S ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove clear (CHead x0 (Bind b) t) c0
we proved clear (CHead x0 (Bind b) t) c0
clear (CHead c (Bind b) t) c0
→∀H7:(eq nat O (s (Bind b) x1)).(clear (CHead x0 (Bind b) t) c0)
assume f: F
suppose H6: clear (CHead c (Flat f) t) c0
suppose H7: eq nat O (s (Flat f) x1)
(H8)
consider H7
we proved eq nat O (s (Flat f) x1)
that is equivalent to eq nat O x1
by (eq_ind_r . . . H5 . previous)
csubst0 O v c x0
end of H8
by (clear_gen_flat . . . . H6)
we proved clear c c0
by (H . . H8 . previous)
we proved clear x0 c0
by (clear_flat . . previous . .)
we proved clear (CHead x0 (Flat f) t) c0
∀H6:clear (CHead c (Flat f) t) c0
.∀H7:(eq nat O (s (Flat f) x1)).(clear (CHead x0 (Flat f) t) c0)
by (previous . H1 H3)
we proved clear (CHead x0 k t) c0
by (eq_ind_r . . . previous . H4)
clear c2 c0
clear c2 c0
case or3_intro2 : H2:ex4_3 T C nat λ:T.λ:C.λj:nat.eq nat O (s k j) λu2:T.λc3:C.λ:nat.eq C c2 (CHead c3 k u2) λu2:T.λ:C.λj:nat.subst0 j v t u2 λ:T.λc3:C.λj:nat.csubst0 j v c c3 ⇒
the thesis becomes clear c2 c0
we proceed by induction on H2 to prove clear c2 c0
case ex4_3_intro : x0:T x1:C x2:nat H3:eq nat O (s k x2) H4:eq C c2 (CHead x1 k x0) H5:subst0 x2 v t x0 H6:csubst0 x2 v c x1 ⇒
the thesis becomes clear c2 c0
assume b: B
suppose : clear (CHead c (Bind b) t) c0
suppose H8: eq nat O (s (Bind b) x2)
(H9)
consider H8
we proved eq nat O (s (Bind b) x2)
that is equivalent to eq nat O (S x2)
we proceed by induction on the previous result to prove <λ:nat.Prop> CASE S x2 OF O⇒True | S ⇒False
case refl_equal : ⇒
the thesis becomes <λ:nat.Prop> CASE O OF O⇒True | S ⇒False
consider I
we proved True
<λ:nat.Prop> CASE O OF O⇒True | S ⇒False
<λ:nat.Prop> CASE S x2 OF O⇒True | S ⇒False
end of H9
consider H9
we proved <λ:nat.Prop> CASE S x2 OF O⇒True | S ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove clear (CHead x1 (Bind b) x0) c0
we proved clear (CHead x1 (Bind b) x0) c0
clear (CHead c (Bind b) t) c0
→∀H8:(eq nat O (s (Bind b) x2)).(clear (CHead x1 (Bind b) x0) c0)
assume f: F
suppose H7: clear (CHead c (Flat f) t) c0
suppose H8: eq nat O (s (Flat f) x2)
(H9)
consider H8
we proved eq nat O (s (Flat f) x2)
that is equivalent to eq nat O x2
by (eq_ind_r . . . H6 . previous)
csubst0 O v c x1
end of H9
by (clear_gen_flat . . . . H7)
we proved clear c c0
by (H . . H9 . previous)
we proved clear x1 c0
by (clear_flat . . previous . .)
we proved clear (CHead x1 (Flat f) x0) c0
∀H7:clear (CHead c (Flat f) t) c0
.∀H8:(eq nat O (s (Flat f) x2)).(clear (CHead x1 (Flat f) x0) c0)
by (previous . H1 H3)
we proved clear (CHead x1 k x0) c0
by (eq_ind_r . . . previous . H4)
clear c2 c0
clear c2 c0
we proved clear c2 c0
∀c2:C.∀v:T.∀H0:(csubst0 O v (CHead c k t) c2).∀c0:C.∀H1:(clear (CHead c k t) c0).(clear c2 c0)
we proved ∀c2:C.∀v:T.(csubst0 O v c1 c2)→∀c0:C.(clear c1 c0)→(clear c2 c0)
we proved ∀c1:C.∀c2:C.∀v:T.(csubst0 O v c1 c2)→∀c0:C.(clear c1 c0)→(clear c2 c0)