DEFINITION csubst0_clear_O_back()
TYPE =
∀c1:C.∀c2:C.∀v:T.(csubst0 O v c1 c2)→∀c:C.(clear c2 c)→(clear c1 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 c2 c0)→(clear c1 c0)
case CSort : n:nat ⇒
the thesis becomes ∀c2:C.∀v:T.∀H:(csubst0 O v (CSort n) c2).∀c:C.(clear c2 c)→(clear (CSort n) c)
assume c2: C
assume v: T
suppose H: csubst0 O v (CSort n) c2
assume c: C
suppose : clear c2 c
by (csubst0_gen_sort . . . . H .)
we proved clear (CSort n) c
∀c2:C.∀v:T.∀H:(csubst0 O v (CSort n) c2).∀c:C.(clear c2 c)→(clear (CSort n) 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 c2 c0).(clear (CHead c k t) c0)
(H) by induction hypothesis we know ∀c2:C.∀v:T.(csubst0 O v c c2)→∀c0:C.(clear c2 c0)→(clear c c0)
assume c2: C
assume v: T
suppose H0: csubst0 O v (CHead c k t) c2
assume c0: C
suppose H1: clear c2 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 (CHead c k t) 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 (CHead c k t) c0
we proceed by induction on H2 to prove clear (CHead c k t) 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 (CHead c k t) c0
(H6)
we proceed by induction on H4 to prove clear (CHead c k x0) c0
case refl_equal : ⇒
the thesis becomes the hypothesis H1
clear (CHead c k x0) c0
end of H6
assume b: B
suppose H7: eq nat O (s (Bind b) x1)
suppose : clear (CHead c (Bind b) x0) c0
(H9)
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 H9
consider H9
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) t) c0
we proved clear (CHead c (Bind b) t) c0
∀H7:eq nat O (s (Bind b) x1)
.clear (CHead c (Bind b) x0) c0
→clear (CHead c (Bind b) t) c0
assume f: F
suppose H7: eq nat O (s (Flat f) x1)
suppose H8: clear (CHead c (Flat f) x0) c0
by (clear_gen_flat . . . . H8)
we proved clear c c0
by (clear_flat . . previous . .)
we proved clear (CHead c (Flat f) t) c0
∀H7:eq nat O (s (Flat f) x1)
.∀H8:(clear (CHead c (Flat f) x0) c0).(clear (CHead c (Flat f) t) c0)
by (previous . H3 H6)
clear (CHead c k t) c0
clear (CHead c k t) 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 (CHead c k t) c0
we proceed by induction on H2 to prove clear (CHead c k t) 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 (CHead c k t) c0
(H6)
we proceed by induction on H4 to prove clear (CHead x0 k t) c0
case refl_equal : ⇒
the thesis becomes the hypothesis H1
clear (CHead x0 k t) c0
end of H6
assume b: B
suppose H7: eq nat O (s (Bind b) x1)
suppose : clear (CHead x0 (Bind b) t) c0
(H9)
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 H9
consider H9
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) t) c0
we proved clear (CHead c (Bind b) t) c0
∀H7:eq nat O (s (Bind b) x1)
.clear (CHead x0 (Bind b) t) c0
→clear (CHead c (Bind b) t) c0
assume f: F
suppose H7: eq nat O (s (Flat f) x1)
suppose H8: clear (CHead x0 (Flat f) t) c0
(H9)
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 H9
by (clear_gen_flat . . . . H8)
we proved clear x0 c0
by (H . . H9 . previous)
we proved clear c c0
by (clear_flat . . previous . .)
we proved clear (CHead c (Flat f) t) c0
∀H7:eq nat O (s (Flat f) x1)
.∀H8:(clear (CHead x0 (Flat f) t) c0).(clear (CHead c (Flat f) t) c0)
by (previous . H3 H6)
clear (CHead c k t) c0
clear (CHead c k t) 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 (CHead c k t) c0
we proceed by induction on H2 to prove clear (CHead c k t) 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 (CHead c k t) c0
(H7)
we proceed by induction on H4 to prove clear (CHead x1 k x0) c0
case refl_equal : ⇒
the thesis becomes the hypothesis H1
clear (CHead x1 k x0) c0
end of H7
assume b: B
suppose H8: eq nat O (s (Bind b) x2)
suppose : clear (CHead x1 (Bind b) x0) c0
(H10)
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 H10
consider H10
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 c (Bind b) t) c0
we proved clear (CHead c (Bind b) t) c0
∀H8:eq nat O (s (Bind b) x2)
.(clear (CHead x1 (Bind b) x0) c0)→(clear (CHead c (Bind b) t) c0)
assume f: F
suppose H8: eq nat O (s (Flat f) x2)
suppose H9: clear (CHead x1 (Flat f) x0) c0
(H10)
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 H10
by (clear_gen_flat . . . . H9)
we proved clear x1 c0
by (H . . H10 . previous)
we proved clear c c0
by (clear_flat . . previous . .)
we proved clear (CHead c (Flat f) t) c0
∀H8:eq nat O (s (Flat f) x2)
.∀H9:(clear (CHead x1 (Flat f) x0) c0).(clear (CHead c (Flat f) t) c0)
by (previous . H3 H7)
clear (CHead c k t) c0
clear (CHead c k t) c0
we proved clear (CHead c k t) c0
∀c2:C.∀v:T.∀H0:(csubst0 O v (CHead c k t) c2).∀c0:C.∀H1:(clear c2 c0).(clear (CHead c k t) c0)
we proved ∀c2:C.∀v:T.(csubst0 O v c1 c2)→∀c0:C.(clear c2 c0)→(clear c1 c0)
we proved ∀c1:C.∀c2:C.∀v:T.(csubst0 O v c1 c2)→∀c0:C.(clear c2 c0)→(clear c1 c0)