DEFINITION csubst0_clear_trans()
TYPE =
∀c1:C
.∀c2:C
.∀v:T
.∀i:nat
.csubst0 i v c1 c2
→∀e2:C.(clear c2 e2)→(or (clear c1 e2) (ex2 C λe1:C.csubst0 i v e1 e2 λe1:C.clear c1 e1))
BODY =
assume c1: C
assume c2: C
assume v: T
assume i: nat
suppose H: csubst0 i v c1 c2
we proceed by induction on H to prove ∀e2:C.(clear c2 e2)→(or (clear c1 e2) (ex2 C λe1:C.csubst0 i v e1 e2 λe1:C.clear c1 e1))
case csubst0_snd : k:K i0:nat v0:T u1:T u2:T H0:subst0 i0 v0 u1 u2 c:C ⇒
the thesis becomes
∀e2:C
.∀H1:clear (CHead c k u2) e2
.or (clear (CHead c k u1) e2) (ex2 C λe1:C.csubst0 (s k i0) v0 e1 e2 λe1:C.clear (CHead c k u1) e1)
assume e2: C
suppose H1: clear (CHead c k u2) e2
assume b: B
suppose H2: clear (CHead c (Bind b) u2) e2
(h1)
(h1)
by (csubst0_snd_bind . . . . . H0 .)
csubst0 (S i0) v0 (CHead c (Bind b) u1) (CHead c (Bind b) u2)
end of h1
(h2)
by (clear_bind . . .)
clear (CHead c (Bind b) u1) (CHead c (Bind b) u1)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2 C λe1:C.csubst0 (S i0) v0 e1 (CHead c (Bind b) u2) λe1:C.clear (CHead c (Bind b) u1) e1
by (or_intror . . previous)
we proved
or
clear (CHead c (Bind b) u1) (CHead c (Bind b) u2)
ex2 C λe1:C.csubst0 (S i0) v0 e1 (CHead c (Bind b) u2) λe1:C.clear (CHead c (Bind b) u1) e1
or
clear (CHead c (Bind b) u1) (CHead c (Bind b) u2)
ex2
C
λe1:C.csubst0 (s (Bind b) i0) v0 e1 (CHead c (Bind b) u2)
λe1:C.clear (CHead c (Bind b) u1) e1
end of h1
(h2)
by (clear_gen_bind . . . . H2)
eq C e2 (CHead c (Bind b) u2)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
or
clear (CHead c (Bind b) u1) e2
ex2 C λe1:C.csubst0 (s (Bind b) i0) v0 e1 e2 λe1:C.clear (CHead c (Bind b) u1) e1
∀H2:clear (CHead c (Bind b) u2) e2
.or
clear (CHead c (Bind b) u1) e2
ex2 C λe1:C.csubst0 (s (Bind b) i0) v0 e1 e2 λe1:C.clear (CHead c (Bind b) u1) e1
assume f: F
suppose H2: clear (CHead c (Flat f) u2) e2
by (clear_gen_flat . . . . H2)
we proved clear c e2
by (clear_flat . . previous . .)
we proved clear (CHead c (Flat f) u1) e2
by (or_introl . . previous)
we proved
or
clear (CHead c (Flat f) u1) e2
ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear (CHead c (Flat f) u1) e1
that is equivalent to
or
clear (CHead c (Flat f) u1) e2
ex2 C λe1:C.csubst0 (s (Flat f) i0) v0 e1 e2 λe1:C.clear (CHead c (Flat f) u1) e1
∀H2:clear (CHead c (Flat f) u2) e2
.or
clear (CHead c (Flat f) u1) e2
ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear (CHead c (Flat f) u1) e1
by (previous . H1)
we proved
or (clear (CHead c k u1) e2) (ex2 C λe1:C.csubst0 (s k i0) v0 e1 e2 λe1:C.clear (CHead c k u1) e1)
∀e2:C
.∀H1:clear (CHead c k u2) e2
.or (clear (CHead c k u1) e2) (ex2 C λe1:C.csubst0 (s k i0) v0 e1 e2 λe1:C.clear (CHead c k u1) e1)
case csubst0_fst : k:K i0:nat c3:C c4:C v0:T H0:csubst0 i0 v0 c3 c4 u:T ⇒
the thesis becomes
∀e2:C
.∀H2:clear (CHead c4 k u) e2
.or (clear (CHead c3 k u) e2) (ex2 C λe1:C.csubst0 (s k i0) v0 e1 e2 λe1:C.clear (CHead c3 k u) e1)
(H1) by induction hypothesis we know ∀e2:C.(clear c4 e2)→(or (clear c3 e2) (ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear c3 e1))
assume e2: C
suppose H2: clear (CHead c4 k u) e2
assume b: B
suppose H3: clear (CHead c4 (Bind b) u) e2
(h1)
(h1)
by (csubst0_fst_bind . . . . . H0 .)
csubst0 (S i0) v0 (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)
we proved
ex2 C λe1:C.csubst0 (S i0) v0 e1 (CHead c4 (Bind b) u) λe1:C.clear (CHead c3 (Bind b) u) e1
by (or_intror . . previous)
we proved
or
clear (CHead c3 (Bind b) u) (CHead c4 (Bind b) u)
ex2 C λe1:C.csubst0 (S i0) v0 e1 (CHead c4 (Bind b) u) λe1:C.clear (CHead c3 (Bind b) u) e1
or
clear (CHead c3 (Bind b) u) (CHead c4 (Bind b) u)
ex2
C
λe1:C.csubst0 (s (Bind b) i0) v0 e1 (CHead c4 (Bind b) u)
λe1:C.clear (CHead c3 (Bind b) u) e1
end of h1
(h2)
by (clear_gen_bind . . . . H3)
eq C e2 (CHead c4 (Bind b) u)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
or
clear (CHead c3 (Bind b) u) e2
ex2 C λe1:C.csubst0 (s (Bind b) i0) v0 e1 e2 λe1:C.clear (CHead c3 (Bind b) u) e1
∀H3:clear (CHead c4 (Bind b) u) e2
.or
clear (CHead c3 (Bind b) u) e2
ex2 C λe1:C.csubst0 (s (Bind b) i0) v0 e1 e2 λe1:C.clear (CHead c3 (Bind b) u) e1
assume f: F
suppose H3: clear (CHead c4 (Flat f) u) e2
(H_x)
by (clear_gen_flat . . . . H3)
we proved clear c4 e2
by (H1 . previous)
or (clear c3 e2) (ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear c3 e1)
end of H_x
(H4) consider H_x
we proceed by induction on H4 to prove
or
clear (CHead c3 (Flat f) u) e2
ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear (CHead c3 (Flat f) u) e1
case or_introl : H5:clear c3 e2 ⇒
the thesis becomes
or
clear (CHead c3 (Flat f) u) e2
ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear (CHead c3 (Flat f) u) e1
by (clear_flat . . H5 . .)
we proved clear (CHead c3 (Flat f) u) e2
by (or_introl . . previous)
or
clear (CHead c3 (Flat f) u) e2
ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear (CHead c3 (Flat f) u) e1
case or_intror : H5:ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear c3 e1 ⇒
the thesis becomes
or
clear (CHead c3 (Flat f) u) e2
ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear (CHead c3 (Flat f) u) e1
we proceed by induction on H5 to prove
or
clear (CHead c3 (Flat f) u) e2
ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear (CHead c3 (Flat f) u) e1
case ex_intro2 : x:C H6:csubst0 i0 v0 x e2 H7:clear c3 x ⇒
the thesis becomes
or
clear (CHead c3 (Flat f) u) e2
ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear (CHead c3 (Flat f) u) e1
by (clear_flat . . H7 . .)
we proved clear (CHead c3 (Flat f) u) x
by (ex_intro2 . . . . H6 previous)
we proved ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear (CHead c3 (Flat f) u) e1
by (or_intror . . previous)
or
clear (CHead c3 (Flat f) u) e2
ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear (CHead c3 (Flat f) u) e1
or
clear (CHead c3 (Flat f) u) e2
ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear (CHead c3 (Flat f) u) e1
we proved
or
clear (CHead c3 (Flat f) u) e2
ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear (CHead c3 (Flat f) u) e1
that is equivalent to
or
clear (CHead c3 (Flat f) u) e2
ex2 C λe1:C.csubst0 (s (Flat f) i0) v0 e1 e2 λe1:C.clear (CHead c3 (Flat f) u) e1
∀H3:clear (CHead c4 (Flat f) u) e2
.or
clear (CHead c3 (Flat f) u) e2
ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear (CHead c3 (Flat f) u) e1
by (previous . H2)
we proved
or (clear (CHead c3 k u) e2) (ex2 C λe1:C.csubst0 (s k i0) v0 e1 e2 λe1:C.clear (CHead c3 k u) e1)
∀e2:C
.∀H2:clear (CHead c4 k u) e2
.or (clear (CHead c3 k u) e2) (ex2 C λe1:C.csubst0 (s k i0) v0 e1 e2 λe1:C.clear (CHead c3 k u) e1)
case csubst0_both : k:K i0:nat v0:T u1:T u2:T H0:subst0 i0 v0 u1 u2 c3:C c4:C H1:csubst0 i0 v0 c3 c4 ⇒
the thesis becomes
∀e2:C
.∀H3:clear (CHead c4 k u2) e2
.or (clear (CHead c3 k u1) e2) (ex2 C λe1:C.csubst0 (s k i0) v0 e1 e2 λe1:C.clear (CHead c3 k u1) e1)
(H2) by induction hypothesis we know ∀e2:C.(clear c4 e2)→(or (clear c3 e2) (ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear c3 e1))
assume e2: C
suppose H3: clear (CHead c4 k u2) e2
assume b: B
suppose H4: clear (CHead c4 (Bind b) u2) e2
(h1)
(h1)
by (csubst0_both_bind . . . . . H0 . . H1)
csubst0 (S i0) v0 (CHead c3 (Bind b) u1) (CHead c4 (Bind b) u2)
end of h1
(h2)
by (clear_bind . . .)
clear (CHead c3 (Bind b) u1) (CHead c3 (Bind b) u1)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved ex2 C λe1:C.csubst0 (S i0) v0 e1 (CHead c4 (Bind b) u2) λe1:C.clear (CHead c3 (Bind b) u1) e1
by (or_intror . . previous)
we proved
or
clear (CHead c3 (Bind b) u1) (CHead c4 (Bind b) u2)
ex2 C λe1:C.csubst0 (S i0) v0 e1 (CHead c4 (Bind b) u2) λe1:C.clear (CHead c3 (Bind b) u1) e1
or
clear (CHead c3 (Bind b) u1) (CHead c4 (Bind b) u2)
ex2
C
λe1:C.csubst0 (s (Bind b) i0) v0 e1 (CHead c4 (Bind b) u2)
λe1:C.clear (CHead c3 (Bind b) u1) e1
end of h1
(h2)
by (clear_gen_bind . . . . H4)
eq C e2 (CHead c4 (Bind b) u2)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
or
clear (CHead c3 (Bind b) u1) e2
ex2 C λe1:C.csubst0 (s (Bind b) i0) v0 e1 e2 λe1:C.clear (CHead c3 (Bind b) u1) e1
∀H4:clear (CHead c4 (Bind b) u2) e2
.or
clear (CHead c3 (Bind b) u1) e2
ex2 C λe1:C.csubst0 (s (Bind b) i0) v0 e1 e2 λe1:C.clear (CHead c3 (Bind b) u1) e1
assume f: F
suppose H4: clear (CHead c4 (Flat f) u2) e2
(H_x)
by (clear_gen_flat . . . . H4)
we proved clear c4 e2
by (H2 . previous)
or (clear c3 e2) (ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear c3 e1)
end of H_x
(H5) consider H_x
we proceed by induction on H5 to prove
or
clear (CHead c3 (Flat f) u1) e2
ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear (CHead c3 (Flat f) u1) e1
case or_introl : H6:clear c3 e2 ⇒
the thesis becomes
or
clear (CHead c3 (Flat f) u1) e2
ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear (CHead c3 (Flat f) u1) e1
by (clear_flat . . H6 . .)
we proved clear (CHead c3 (Flat f) u1) e2
by (or_introl . . previous)
or
clear (CHead c3 (Flat f) u1) e2
ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear (CHead c3 (Flat f) u1) e1
case or_intror : H6:ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear c3 e1 ⇒
the thesis becomes
or
clear (CHead c3 (Flat f) u1) e2
ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear (CHead c3 (Flat f) u1) e1
we proceed by induction on H6 to prove
or
clear (CHead c3 (Flat f) u1) e2
ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear (CHead c3 (Flat f) u1) e1
case ex_intro2 : x:C H7:csubst0 i0 v0 x e2 H8:clear c3 x ⇒
the thesis becomes
or
clear (CHead c3 (Flat f) u1) e2
ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear (CHead c3 (Flat f) u1) e1
by (clear_flat . . H8 . .)
we proved clear (CHead c3 (Flat f) u1) x
by (ex_intro2 . . . . H7 previous)
we proved ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear (CHead c3 (Flat f) u1) e1
by (or_intror . . previous)
or
clear (CHead c3 (Flat f) u1) e2
ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear (CHead c3 (Flat f) u1) e1
or
clear (CHead c3 (Flat f) u1) e2
ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear (CHead c3 (Flat f) u1) e1
we proved
or
clear (CHead c3 (Flat f) u1) e2
ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear (CHead c3 (Flat f) u1) e1
that is equivalent to
or
clear (CHead c3 (Flat f) u1) e2
ex2 C λe1:C.csubst0 (s (Flat f) i0) v0 e1 e2 λe1:C.clear (CHead c3 (Flat f) u1) e1
∀H4:clear (CHead c4 (Flat f) u2) e2
.or
clear (CHead c3 (Flat f) u1) e2
ex2 C λe1:C.csubst0 i0 v0 e1 e2 λe1:C.clear (CHead c3 (Flat f) u1) e1
by (previous . H3)
we proved or (clear (CHead c3 k u1) e2) (ex2 C λe1:C.csubst0 (s k i0) v0 e1 e2 λe1:C.clear (CHead c3 k u1) e1)
∀e2:C
.∀H3:clear (CHead c4 k u2) e2
.or (clear (CHead c3 k u1) e2) (ex2 C λe1:C.csubst0 (s k i0) v0 e1 e2 λe1:C.clear (CHead c3 k u1) e1)
we proved ∀e2:C.(clear c2 e2)→(or (clear c1 e2) (ex2 C λe1:C.csubst0 i v e1 e2 λe1:C.clear c1 e1))
we proved
∀c1:C
.∀c2:C
.∀v:T
.∀i:nat
.csubst0 i v c1 c2
→∀e2:C.(clear c2 e2)→(or (clear c1 e2) (ex2 C λe1:C.csubst0 i v e1 e2 λe1:C.clear c1 e1))