DEFINITION csubst0_gen_S_bind_2()
TYPE =
∀b:B
.∀x:C
.∀c2:C
.∀v:T
.∀v2:T
.∀i:nat
.csubst0 (S i) v x (CHead c2 (Bind b) v2)
→(or3
ex2 T λv1:T.subst0 i v v1 v2 λv1:T.eq C x (CHead c2 (Bind b) v1)
ex2 C λc1:C.csubst0 i v c1 c2 λc1:C.eq C x (CHead c1 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v v1 v2 λc1:C.λ:T.csubst0 i v c1 c2 λc1:C.λv1:T.eq C x (CHead c1 (Bind b) v1))
BODY =
assume b: B
assume x: C
assume c2: C
assume v: T
assume v2: T
assume i: nat
suppose H: csubst0 (S i) v x (CHead c2 (Bind b) v2)
assume y: C
suppose H0: csubst0 (S i) v x y
assume y0: nat
suppose H1: csubst0 y0 v x y
we proceed by induction on H1 to prove
eq nat y0 (S i)
→(eq C y (CHead c2 (Bind b) v2)
→(or3
ex2 T λv1:T.subst0 i v v1 v2 λv1:T.eq C x (CHead c2 (Bind b) v1)
ex2 C λc1:C.csubst0 i v c1 c2 λc1:C.eq C x (CHead c1 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v v1 v2 λc1:C.λ:T.csubst0 i v c1 c2 λc1:C.λv1:T.eq C x (CHead c1 (Bind b) v1)))
case csubst0_snd : k:K i0:nat v0:T u1:T u2:T H2:subst0 i0 v0 u1 u2 c:C ⇒
the thesis becomes
∀H3:eq nat (s k i0) (S i)
.∀H4:eq C (CHead c k u2) (CHead c2 (Bind b) v2)
.or3
ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C (CHead c k u1) (CHead c2 (Bind b) v1)
ex2 C λc1:C.csubst0 i v0 c1 c2 λc1:C.eq C (CHead c k u1) (CHead c1 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v0 v1 v2 λc1:C.λ:T.csubst0 i v0 c1 c2 λc1:C.λv1:T.eq C (CHead c k u1) (CHead c1 (Bind b) v1)
suppose H3: eq nat (s k i0) (S i)
suppose H4: eq C (CHead c k u2) (CHead c2 (Bind b) v2)
(H5)
by (f_equal . . . . . H4)
we proved
eq
C
<λ:C.C> CASE CHead c k u2 OF CSort ⇒c | CHead c0 ⇒c0
<λ:C.C> CASE CHead c2 (Bind b) v2 OF CSort ⇒c | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒c | CHead c0 ⇒c0 (CHead c k u2)
λe:C.<λ:C.C> CASE e OF CSort ⇒c | CHead c0 ⇒c0 (CHead c2 (Bind b) v2)
end of H5
(h1)
(H6)
by (f_equal . . . . . H4)
we proved
eq
K
<λ:C.K> CASE CHead c k u2 OF CSort ⇒k | CHead k0 ⇒k0
<λ:C.K> CASE CHead c2 (Bind b) v2 OF CSort ⇒k | CHead k0 ⇒k0
eq
K
λe:C.<λ:C.K> CASE e OF CSort ⇒k | CHead k0 ⇒k0 (CHead c k u2)
λe:C.<λ:C.K> CASE e OF CSort ⇒k | CHead k0 ⇒k0 (CHead c2 (Bind b) v2)
end of H6
(h1)
(H7)
by (f_equal . . . . . H4)
we proved
eq
T
<λ:C.T> CASE CHead c k u2 OF CSort ⇒u2 | CHead t⇒t
<λ:C.T> CASE CHead c2 (Bind b) v2 OF CSort ⇒u2 | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u2 | CHead t⇒t (CHead c k u2)
λe:C.<λ:C.T> CASE e OF CSort ⇒u2 | CHead t⇒t (CHead c2 (Bind b) v2)
end of H7
suppose H8: eq K k (Bind b)
suppose H9: eq C c c2
(H10)
consider H7
we proved
eq
T
<λ:C.T> CASE CHead c k u2 OF CSort ⇒u2 | CHead t⇒t
<λ:C.T> CASE CHead c2 (Bind b) v2 OF CSort ⇒u2 | CHead t⇒t
that is equivalent to eq T u2 v2
we proceed by induction on the previous result to prove subst0 i0 v0 u1 v2
case refl_equal : ⇒
the thesis becomes the hypothesis H2
subst0 i0 v0 u1 v2
end of H10
(H11)
we proceed by induction on H8 to prove eq nat (s (Bind b) i0) (S i)
case refl_equal : ⇒
the thesis becomes the hypothesis H3
eq nat (s (Bind b) i0) (S i)
end of H11
(H12)
consider H11
we proved eq nat (s (Bind b) i0) (S i)
that is equivalent to eq nat (S i0) (S i)
by (f_equal . . . . . previous)
we proved
eq
nat
<λ:nat.nat> CASE S i0 OF O⇒i0 | S n⇒n
<λ:nat.nat> CASE S i OF O⇒i0 | S n⇒n
eq
nat
λe:nat.<λ:nat.nat> CASE e OF O⇒i0 | S n⇒n (S i0)
λe:nat.<λ:nat.nat> CASE e OF O⇒i0 | S n⇒n (S i)
end of H12
(H13)
consider H12
we proved
eq
nat
<λ:nat.nat> CASE S i0 OF O⇒i0 | S n⇒n
<λ:nat.nat> CASE S i OF O⇒i0 | S n⇒n
that is equivalent to eq nat i0 i
we proceed by induction on the previous result to prove subst0 i v0 u1 v2
case refl_equal : ⇒
the thesis becomes the hypothesis H10
subst0 i v0 u1 v2
end of H13
by (refl_equal . .)
we proved eq C (CHead c2 (Bind b) u1) (CHead c2 (Bind b) u1)
by (ex_intro2 . . . . H13 previous)
we proved ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C (CHead c2 (Bind b) u1) (CHead c2 (Bind b) v1)
by (or3_intro0 . . . previous)
we proved
or3
ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C (CHead c2 (Bind b) u1) (CHead c2 (Bind b) v1)
ex2 C λc1:C.csubst0 i v0 c1 c2 λc1:C.eq C (CHead c2 (Bind b) u1) (CHead c1 (Bind b) v2)
ex3_2
C
T
λ:C.λv1:T.subst0 i v0 v1 v2
λc1:C.λ:T.csubst0 i v0 c1 c2
λc1:C.λv1:T.eq C (CHead c2 (Bind b) u1) (CHead c1 (Bind b) v1)
by (eq_ind_r . . . previous . H8)
we proved
or3
ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C (CHead c2 k u1) (CHead c2 (Bind b) v1)
ex2 C λc1:C.csubst0 i v0 c1 c2 λc1:C.eq C (CHead c2 k u1) (CHead c1 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v0 v1 v2 λc1:C.λ:T.csubst0 i v0 c1 c2 λc1:C.λv1:T.eq C (CHead c2 k u1) (CHead c1 (Bind b) v1)
by (eq_ind_r . . . previous . H9)
we proved
or3
ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C (CHead c k u1) (CHead c2 (Bind b) v1)
ex2 C λc1:C.csubst0 i v0 c1 c2 λc1:C.eq C (CHead c k u1) (CHead c1 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v0 v1 v2 λc1:C.λ:T.csubst0 i v0 c1 c2 λc1:C.λv1:T.eq C (CHead c k u1) (CHead c1 (Bind b) v1)
eq K k (Bind b)
→(eq C c c2
→(or3
ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C (CHead c k u1) (CHead c2 (Bind b) v1)
ex2 C λc1:C.csubst0 i v0 c1 c2 λc1:C.eq C (CHead c k u1) (CHead c1 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v0 v1 v2 λc1:C.λ:T.csubst0 i v0 c1 c2 λc1:C.λv1:T.eq C (CHead c k u1) (CHead c1 (Bind b) v1)))
end of h1
(h2)
consider H6
we proved
eq
K
<λ:C.K> CASE CHead c k u2 OF CSort ⇒k | CHead k0 ⇒k0
<λ:C.K> CASE CHead c2 (Bind b) v2 OF CSort ⇒k | CHead k0 ⇒k0
eq K k (Bind b)
end of h2
by (h1 h2)
eq C c c2
→(or3
ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C (CHead c k u1) (CHead c2 (Bind b) v1)
ex2 C λc1:C.csubst0 i v0 c1 c2 λc1:C.eq C (CHead c k u1) (CHead c1 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v0 v1 v2 λc1:C.λ:T.csubst0 i v0 c1 c2 λc1:C.λv1:T.eq C (CHead c k u1) (CHead c1 (Bind b) v1))
end of h1
(h2)
consider H5
we proved
eq
C
<λ:C.C> CASE CHead c k u2 OF CSort ⇒c | CHead c0 ⇒c0
<λ:C.C> CASE CHead c2 (Bind b) v2 OF CSort ⇒c | CHead c0 ⇒c0
eq C c c2
end of h2
by (h1 h2)
we proved
or3
ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C (CHead c k u1) (CHead c2 (Bind b) v1)
ex2 C λc1:C.csubst0 i v0 c1 c2 λc1:C.eq C (CHead c k u1) (CHead c1 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v0 v1 v2 λc1:C.λ:T.csubst0 i v0 c1 c2 λc1:C.λv1:T.eq C (CHead c k u1) (CHead c1 (Bind b) v1)
∀H3:eq nat (s k i0) (S i)
.∀H4:eq C (CHead c k u2) (CHead c2 (Bind b) v2)
.or3
ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C (CHead c k u1) (CHead c2 (Bind b) v1)
ex2 C λc1:C.csubst0 i v0 c1 c2 λc1:C.eq C (CHead c k u1) (CHead c1 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v0 v1 v2 λc1:C.λ:T.csubst0 i v0 c1 c2 λc1:C.λv1:T.eq C (CHead c k u1) (CHead c1 (Bind b) v1)
case csubst0_fst : k:K i0:nat c1:C c0:C v0:T H2:csubst0 i0 v0 c1 c0 u:T ⇒
the thesis becomes
∀H4:eq nat (s k i0) (S i)
.∀H5:eq C (CHead c0 k u) (CHead c2 (Bind b) v2)
.or3
ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C (CHead c1 k u) (CHead c2 (Bind b) v1)
ex2 C λc3:C.csubst0 i v0 c3 c2 λc3:C.eq C (CHead c1 k u) (CHead c3 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v0 v1 v2 λc3:C.λ:T.csubst0 i v0 c3 c2 λc3:C.λv1:T.eq C (CHead c1 k u) (CHead c3 (Bind b) v1)
(H3) by induction hypothesis we know
eq nat i0 (S i)
→(eq C c0 (CHead c2 (Bind b) v2)
→(or3
ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C c1 (CHead c2 (Bind b) v1)
ex2 C λc3:C.csubst0 i v0 c3 c2 λc3:C.eq C c1 (CHead c3 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v0 v1 v2 λc3:C.λ:T.csubst0 i v0 c3 c2 λc3:C.λv1:T.eq C c1 (CHead c3 (Bind b) v1)))
suppose H4: eq nat (s k i0) (S i)
suppose H5: eq C (CHead c0 k u) (CHead c2 (Bind b) v2)
(H6)
by (f_equal . . . . . H5)
we proved
eq
C
<λ:C.C> CASE CHead c0 k u OF CSort ⇒c0 | CHead c ⇒c
<λ:C.C> CASE CHead c2 (Bind b) v2 OF CSort ⇒c0 | CHead c ⇒c
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒c0 | CHead c ⇒c (CHead c0 k u)
λe:C.<λ:C.C> CASE e OF CSort ⇒c0 | CHead c ⇒c (CHead c2 (Bind b) v2)
end of H6
(h1)
(H7)
by (f_equal . . . . . H5)
we proved
eq
K
<λ:C.K> CASE CHead c0 k u OF CSort ⇒k | CHead k0 ⇒k0
<λ:C.K> CASE CHead c2 (Bind b) v2 OF CSort ⇒k | CHead k0 ⇒k0
eq
K
λe:C.<λ:C.K> CASE e OF CSort ⇒k | CHead k0 ⇒k0 (CHead c0 k u)
λe:C.<λ:C.K> CASE e OF CSort ⇒k | CHead k0 ⇒k0 (CHead c2 (Bind b) v2)
end of H7
(h1)
(H8)
by (f_equal . . . . . H5)
we proved
eq
T
<λ:C.T> CASE CHead c0 k u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead c2 (Bind b) v2 OF CSort ⇒u | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t (CHead c0 k u)
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t (CHead c2 (Bind b) v2)
end of H8
suppose H9: eq K k (Bind b)
suppose H10: eq C c0 c2
(h1)
(H11)
we proceed by induction on H10 to prove
eq nat i0 (S i)
→(eq C c2 (CHead c2 (Bind b) v2)
→(or3
ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C c1 (CHead c2 (Bind b) v1)
ex2 C λc3:C.csubst0 i v0 c3 c2 λc3:C.eq C c1 (CHead c3 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v0 v1 v2 λc3:C.λ:T.csubst0 i v0 c3 c2 λc3:C.λv1:T.eq C c1 (CHead c3 (Bind b) v1)))
case refl_equal : ⇒
the thesis becomes the hypothesis H3
eq nat i0 (S i)
→(eq C c2 (CHead c2 (Bind b) v2)
→(or3
ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C c1 (CHead c2 (Bind b) v1)
ex2 C λc3:C.csubst0 i v0 c3 c2 λc3:C.eq C c1 (CHead c3 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v0 v1 v2 λc3:C.λ:T.csubst0 i v0 c3 c2 λc3:C.λv1:T.eq C c1 (CHead c3 (Bind b) v1)))
end of H11
(H12)
we proceed by induction on H10 to prove csubst0 i0 v0 c1 c2
case refl_equal : ⇒
the thesis becomes the hypothesis H2
csubst0 i0 v0 c1 c2
end of H12
(H13)
we proceed by induction on H9 to prove eq nat (s (Bind b) i0) (S i)
case refl_equal : ⇒
the thesis becomes the hypothesis H4
eq nat (s (Bind b) i0) (S i)
end of H13
(H14)
consider H13
we proved eq nat (s (Bind b) i0) (S i)
that is equivalent to eq nat (S i0) (S i)
by (f_equal . . . . . previous)
we proved
eq
nat
<λ:nat.nat> CASE S i0 OF O⇒i0 | S n⇒n
<λ:nat.nat> CASE S i OF O⇒i0 | S n⇒n
eq
nat
λe:nat.<λ:nat.nat> CASE e OF O⇒i0 | S n⇒n (S i0)
λe:nat.<λ:nat.nat> CASE e OF O⇒i0 | S n⇒n (S i)
end of H14
(H16)
consider H14
we proved
eq
nat
<λ:nat.nat> CASE S i0 OF O⇒i0 | S n⇒n
<λ:nat.nat> CASE S i OF O⇒i0 | S n⇒n
that is equivalent to eq nat i0 i
we proceed by induction on the previous result to prove csubst0 i v0 c1 c2
case refl_equal : ⇒
the thesis becomes the hypothesis H12
csubst0 i v0 c1 c2
end of H16
by (refl_equal . .)
we proved eq C (CHead c1 (Bind b) v2) (CHead c1 (Bind b) v2)
by (ex_intro2 . . . . H16 previous)
we proved ex2 C λc3:C.csubst0 i v0 c3 c2 λc3:C.eq C (CHead c1 (Bind b) v2) (CHead c3 (Bind b) v2)
by (or3_intro1 . . . previous)
we proved
or3
ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C (CHead c1 (Bind b) v2) (CHead c2 (Bind b) v1)
ex2 C λc3:C.csubst0 i v0 c3 c2 λc3:C.eq C (CHead c1 (Bind b) v2) (CHead c3 (Bind b) v2)
ex3_2
C
T
λ:C.λv1:T.subst0 i v0 v1 v2
λc3:C.λ:T.csubst0 i v0 c3 c2
λc3:C.λv1:T.eq C (CHead c1 (Bind b) v2) (CHead c3 (Bind b) v1)
by (eq_ind_r . . . previous . H9)
or3
ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C (CHead c1 k v2) (CHead c2 (Bind b) v1)
ex2 C λc3:C.csubst0 i v0 c3 c2 λc3:C.eq C (CHead c1 k v2) (CHead c3 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v0 v1 v2 λc3:C.λ:T.csubst0 i v0 c3 c2 λc3:C.λv1:T.eq C (CHead c1 k v2) (CHead c3 (Bind b) v1)
end of h1
(h2)
consider H8
we proved
eq
T
<λ:C.T> CASE CHead c0 k u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead c2 (Bind b) v2 OF CSort ⇒u | CHead t⇒t
eq T u v2
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
or3
ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C (CHead c1 k u) (CHead c2 (Bind b) v1)
ex2 C λc3:C.csubst0 i v0 c3 c2 λc3:C.eq C (CHead c1 k u) (CHead c3 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v0 v1 v2 λc3:C.λ:T.csubst0 i v0 c3 c2 λc3:C.λv1:T.eq C (CHead c1 k u) (CHead c3 (Bind b) v1)
eq K k (Bind b)
→(eq C c0 c2
→(or3
ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C (CHead c1 k u) (CHead c2 (Bind b) v1)
ex2 C λc3:C.csubst0 i v0 c3 c2 λc3:C.eq C (CHead c1 k u) (CHead c3 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v0 v1 v2 λc3:C.λ:T.csubst0 i v0 c3 c2 λc3:C.λv1:T.eq C (CHead c1 k u) (CHead c3 (Bind b) v1)))
end of h1
(h2)
consider H7
we proved
eq
K
<λ:C.K> CASE CHead c0 k u OF CSort ⇒k | CHead k0 ⇒k0
<λ:C.K> CASE CHead c2 (Bind b) v2 OF CSort ⇒k | CHead k0 ⇒k0
eq K k (Bind b)
end of h2
by (h1 h2)
eq C c0 c2
→(or3
ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C (CHead c1 k u) (CHead c2 (Bind b) v1)
ex2 C λc3:C.csubst0 i v0 c3 c2 λc3:C.eq C (CHead c1 k u) (CHead c3 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v0 v1 v2 λc3:C.λ:T.csubst0 i v0 c3 c2 λc3:C.λv1:T.eq C (CHead c1 k u) (CHead c3 (Bind b) v1))
end of h1
(h2)
consider H6
we proved
eq
C
<λ:C.C> CASE CHead c0 k u OF CSort ⇒c0 | CHead c ⇒c
<λ:C.C> CASE CHead c2 (Bind b) v2 OF CSort ⇒c0 | CHead c ⇒c
eq C c0 c2
end of h2
by (h1 h2)
we proved
or3
ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C (CHead c1 k u) (CHead c2 (Bind b) v1)
ex2 C λc3:C.csubst0 i v0 c3 c2 λc3:C.eq C (CHead c1 k u) (CHead c3 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v0 v1 v2 λc3:C.λ:T.csubst0 i v0 c3 c2 λc3:C.λv1:T.eq C (CHead c1 k u) (CHead c3 (Bind b) v1)
∀H4:eq nat (s k i0) (S i)
.∀H5:eq C (CHead c0 k u) (CHead c2 (Bind b) v2)
.or3
ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C (CHead c1 k u) (CHead c2 (Bind b) v1)
ex2 C λc3:C.csubst0 i v0 c3 c2 λc3:C.eq C (CHead c1 k u) (CHead c3 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v0 v1 v2 λc3:C.λ:T.csubst0 i v0 c3 c2 λc3:C.λv1:T.eq C (CHead c1 k u) (CHead c3 (Bind b) v1)
case csubst0_both : k:K i0:nat v0:T u1:T u2:T H2:subst0 i0 v0 u1 u2 c1:C c0:C H3:csubst0 i0 v0 c1 c0 ⇒
the thesis becomes
∀H5:eq nat (s k i0) (S i)
.∀H6:eq C (CHead c0 k u2) (CHead c2 (Bind b) v2)
.or3
ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C (CHead c1 k u1) (CHead c2 (Bind b) v1)
ex2 C λc3:C.csubst0 i v0 c3 c2 λc3:C.eq C (CHead c1 k u1) (CHead c3 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v0 v1 v2 λc3:C.λ:T.csubst0 i v0 c3 c2 λc3:C.λv1:T.eq C (CHead c1 k u1) (CHead c3 (Bind b) v1)
(H4) by induction hypothesis we know
eq nat i0 (S i)
→(eq C c0 (CHead c2 (Bind b) v2)
→(or3
ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C c1 (CHead c2 (Bind b) v1)
ex2 C λc3:C.csubst0 i v0 c3 c2 λc3:C.eq C c1 (CHead c3 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v0 v1 v2 λc3:C.λ:T.csubst0 i v0 c3 c2 λc3:C.λv1:T.eq C c1 (CHead c3 (Bind b) v1)))
suppose H5: eq nat (s k i0) (S i)
suppose H6: eq C (CHead c0 k u2) (CHead c2 (Bind b) v2)
(H7)
by (f_equal . . . . . H6)
we proved
eq
C
<λ:C.C> CASE CHead c0 k u2 OF CSort ⇒c0 | CHead c ⇒c
<λ:C.C> CASE CHead c2 (Bind b) v2 OF CSort ⇒c0 | CHead c ⇒c
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒c0 | CHead c ⇒c (CHead c0 k u2)
λe:C.<λ:C.C> CASE e OF CSort ⇒c0 | CHead c ⇒c (CHead c2 (Bind b) v2)
end of H7
(h1)
(H8)
by (f_equal . . . . . H6)
we proved
eq
K
<λ:C.K> CASE CHead c0 k u2 OF CSort ⇒k | CHead k0 ⇒k0
<λ:C.K> CASE CHead c2 (Bind b) v2 OF CSort ⇒k | CHead k0 ⇒k0
eq
K
λe:C.<λ:C.K> CASE e OF CSort ⇒k | CHead k0 ⇒k0 (CHead c0 k u2)
λe:C.<λ:C.K> CASE e OF CSort ⇒k | CHead k0 ⇒k0 (CHead c2 (Bind b) v2)
end of H8
(h1)
(H9)
by (f_equal . . . . . H6)
we proved
eq
T
<λ:C.T> CASE CHead c0 k u2 OF CSort ⇒u2 | CHead t⇒t
<λ:C.T> CASE CHead c2 (Bind b) v2 OF CSort ⇒u2 | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u2 | CHead t⇒t (CHead c0 k u2)
λe:C.<λ:C.T> CASE e OF CSort ⇒u2 | CHead t⇒t (CHead c2 (Bind b) v2)
end of H9
suppose H10: eq K k (Bind b)
suppose H11: eq C c0 c2
(H12)
we proceed by induction on H11 to prove
eq nat i0 (S i)
→(eq C c2 (CHead c2 (Bind b) v2)
→(or3
ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C c1 (CHead c2 (Bind b) v1)
ex2 C λc3:C.csubst0 i v0 c3 c2 λc3:C.eq C c1 (CHead c3 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v0 v1 v2 λc3:C.λ:T.csubst0 i v0 c3 c2 λc3:C.λv1:T.eq C c1 (CHead c3 (Bind b) v1)))
case refl_equal : ⇒
the thesis becomes the hypothesis H4
eq nat i0 (S i)
→(eq C c2 (CHead c2 (Bind b) v2)
→(or3
ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C c1 (CHead c2 (Bind b) v1)
ex2 C λc3:C.csubst0 i v0 c3 c2 λc3:C.eq C c1 (CHead c3 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v0 v1 v2 λc3:C.λ:T.csubst0 i v0 c3 c2 λc3:C.λv1:T.eq C c1 (CHead c3 (Bind b) v1)))
end of H12
(H13)
we proceed by induction on H11 to prove csubst0 i0 v0 c1 c2
case refl_equal : ⇒
the thesis becomes the hypothesis H3
csubst0 i0 v0 c1 c2
end of H13
(H14)
consider H9
we proved
eq
T
<λ:C.T> CASE CHead c0 k u2 OF CSort ⇒u2 | CHead t⇒t
<λ:C.T> CASE CHead c2 (Bind b) v2 OF CSort ⇒u2 | CHead t⇒t
that is equivalent to eq T u2 v2
we proceed by induction on the previous result to prove subst0 i0 v0 u1 v2
case refl_equal : ⇒
the thesis becomes the hypothesis H2
subst0 i0 v0 u1 v2
end of H14
(H15)
we proceed by induction on H10 to prove eq nat (s (Bind b) i0) (S i)
case refl_equal : ⇒
the thesis becomes the hypothesis H5
eq nat (s (Bind b) i0) (S i)
end of H15
(H16)
consider H15
we proved eq nat (s (Bind b) i0) (S i)
that is equivalent to eq nat (S i0) (S i)
by (f_equal . . . . . previous)
we proved
eq
nat
<λ:nat.nat> CASE S i0 OF O⇒i0 | S n⇒n
<λ:nat.nat> CASE S i OF O⇒i0 | S n⇒n
eq
nat
λe:nat.<λ:nat.nat> CASE e OF O⇒i0 | S n⇒n (S i0)
λe:nat.<λ:nat.nat> CASE e OF O⇒i0 | S n⇒n (S i)
end of H16
(H18)
consider H16
we proved
eq
nat
<λ:nat.nat> CASE S i0 OF O⇒i0 | S n⇒n
<λ:nat.nat> CASE S i OF O⇒i0 | S n⇒n
that is equivalent to eq nat i0 i
we proceed by induction on the previous result to prove csubst0 i v0 c1 c2
case refl_equal : ⇒
the thesis becomes the hypothesis H13
csubst0 i v0 c1 c2
end of H18
(H19)
consider H16
we proved
eq
nat
<λ:nat.nat> CASE S i0 OF O⇒i0 | S n⇒n
<λ:nat.nat> CASE S i OF O⇒i0 | S n⇒n
that is equivalent to eq nat i0 i
we proceed by induction on the previous result to prove subst0 i v0 u1 v2
case refl_equal : ⇒
the thesis becomes the hypothesis H14
subst0 i v0 u1 v2
end of H19
by (refl_equal . .)
we proved eq C (CHead c1 (Bind b) u1) (CHead c1 (Bind b) u1)
by (ex3_2_intro . . . . . . . H19 H18 previous)
we proved
ex3_2
C
T
λ:C.λv1:T.subst0 i v0 v1 v2
λc3:C.λ:T.csubst0 i v0 c3 c2
λc3:C.λv1:T.eq C (CHead c1 (Bind b) u1) (CHead c3 (Bind b) v1)
by (or3_intro2 . . . previous)
we proved
or3
ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C (CHead c1 (Bind b) u1) (CHead c2 (Bind b) v1)
ex2 C λc3:C.csubst0 i v0 c3 c2 λc3:C.eq C (CHead c1 (Bind b) u1) (CHead c3 (Bind b) v2)
ex3_2
C
T
λ:C.λv1:T.subst0 i v0 v1 v2
λc3:C.λ:T.csubst0 i v0 c3 c2
λc3:C.λv1:T.eq C (CHead c1 (Bind b) u1) (CHead c3 (Bind b) v1)
by (eq_ind_r . . . previous . H10)
we proved
or3
ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C (CHead c1 k u1) (CHead c2 (Bind b) v1)
ex2 C λc3:C.csubst0 i v0 c3 c2 λc3:C.eq C (CHead c1 k u1) (CHead c3 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v0 v1 v2 λc3:C.λ:T.csubst0 i v0 c3 c2 λc3:C.λv1:T.eq C (CHead c1 k u1) (CHead c3 (Bind b) v1)
eq K k (Bind b)
→(eq C c0 c2
→(or3
ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C (CHead c1 k u1) (CHead c2 (Bind b) v1)
ex2 C λc3:C.csubst0 i v0 c3 c2 λc3:C.eq C (CHead c1 k u1) (CHead c3 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v0 v1 v2 λc3:C.λ:T.csubst0 i v0 c3 c2 λc3:C.λv1:T.eq C (CHead c1 k u1) (CHead c3 (Bind b) v1)))
end of h1
(h2)
consider H8
we proved
eq
K
<λ:C.K> CASE CHead c0 k u2 OF CSort ⇒k | CHead k0 ⇒k0
<λ:C.K> CASE CHead c2 (Bind b) v2 OF CSort ⇒k | CHead k0 ⇒k0
eq K k (Bind b)
end of h2
by (h1 h2)
eq C c0 c2
→(or3
ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C (CHead c1 k u1) (CHead c2 (Bind b) v1)
ex2 C λc3:C.csubst0 i v0 c3 c2 λc3:C.eq C (CHead c1 k u1) (CHead c3 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v0 v1 v2 λc3:C.λ:T.csubst0 i v0 c3 c2 λc3:C.λv1:T.eq C (CHead c1 k u1) (CHead c3 (Bind b) v1))
end of h1
(h2)
consider H7
we proved
eq
C
<λ:C.C> CASE CHead c0 k u2 OF CSort ⇒c0 | CHead c ⇒c
<λ:C.C> CASE CHead c2 (Bind b) v2 OF CSort ⇒c0 | CHead c ⇒c
eq C c0 c2
end of h2
by (h1 h2)
we proved
or3
ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C (CHead c1 k u1) (CHead c2 (Bind b) v1)
ex2 C λc3:C.csubst0 i v0 c3 c2 λc3:C.eq C (CHead c1 k u1) (CHead c3 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v0 v1 v2 λc3:C.λ:T.csubst0 i v0 c3 c2 λc3:C.λv1:T.eq C (CHead c1 k u1) (CHead c3 (Bind b) v1)
∀H5:eq nat (s k i0) (S i)
.∀H6:eq C (CHead c0 k u2) (CHead c2 (Bind b) v2)
.or3
ex2 T λv1:T.subst0 i v0 v1 v2 λv1:T.eq C (CHead c1 k u1) (CHead c2 (Bind b) v1)
ex2 C λc3:C.csubst0 i v0 c3 c2 λc3:C.eq C (CHead c1 k u1) (CHead c3 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v0 v1 v2 λc3:C.λ:T.csubst0 i v0 c3 c2 λc3:C.λv1:T.eq C (CHead c1 k u1) (CHead c3 (Bind b) v1)
we proved
eq nat y0 (S i)
→(eq C y (CHead c2 (Bind b) v2)
→(or3
ex2 T λv1:T.subst0 i v v1 v2 λv1:T.eq C x (CHead c2 (Bind b) v1)
ex2 C λc1:C.csubst0 i v c1 c2 λc1:C.eq C x (CHead c1 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v v1 v2 λc1:C.λ:T.csubst0 i v c1 c2 λc1:C.λv1:T.eq C x (CHead c1 (Bind b) v1)))
we proved
∀y0:nat
.csubst0 y0 v x y
→(eq nat y0 (S i)
→(eq C y (CHead c2 (Bind b) v2)
→(or3
ex2 T λv1:T.subst0 i v v1 v2 λv1:T.eq C x (CHead c2 (Bind b) v1)
ex2 C λc1:C.csubst0 i v c1 c2 λc1:C.eq C x (CHead c1 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v v1 v2 λc1:C.λ:T.csubst0 i v c1 c2 λc1:C.λv1:T.eq C x (CHead c1 (Bind b) v1))))
by (insert_eq . . . . previous H0)
we proved
eq C y (CHead c2 (Bind b) v2)
→(or3
ex2 T λv1:T.subst0 i v v1 v2 λv1:T.eq C x (CHead c2 (Bind b) v1)
ex2 C λc1:C.csubst0 i v c1 c2 λc1:C.eq C x (CHead c1 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v v1 v2 λc1:C.λ:T.csubst0 i v c1 c2 λc1:C.λv1:T.eq C x (CHead c1 (Bind b) v1))
we proved
∀y:C
.csubst0 (S i) v x y
→(eq C y (CHead c2 (Bind b) v2)
→(or3
ex2 T λv1:T.subst0 i v v1 v2 λv1:T.eq C x (CHead c2 (Bind b) v1)
ex2 C λc1:C.csubst0 i v c1 c2 λc1:C.eq C x (CHead c1 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v v1 v2 λc1:C.λ:T.csubst0 i v c1 c2 λc1:C.λv1:T.eq C x (CHead c1 (Bind b) v1)))
by (insert_eq . . . . previous H)
we proved
or3
ex2 T λv1:T.subst0 i v v1 v2 λv1:T.eq C x (CHead c2 (Bind b) v1)
ex2 C λc1:C.csubst0 i v c1 c2 λc1:C.eq C x (CHead c1 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v v1 v2 λc1:C.λ:T.csubst0 i v c1 c2 λc1:C.λv1:T.eq C x (CHead c1 (Bind b) v1)
we proved
∀b:B
.∀x:C
.∀c2:C
.∀v:T
.∀v2:T
.∀i:nat
.csubst0 (S i) v x (CHead c2 (Bind b) v2)
→(or3
ex2 T λv1:T.subst0 i v v1 v2 λv1:T.eq C x (CHead c2 (Bind b) v1)
ex2 C λc1:C.csubst0 i v c1 c2 λc1:C.eq C x (CHead c1 (Bind b) v2)
ex3_2 C T λ:C.λv1:T.subst0 i v v1 v2 λc1:C.λ:T.csubst0 i v c1 c2 λc1:C.λv1:T.eq C x (CHead c1 (Bind b) v1))