DEFINITION csubst0_gen_head()
TYPE =
∀k:K
.∀c1:C
.∀x:C
.∀u1:T
.∀v:T
.∀i:nat
.csubst0 i v (CHead c1 k u1) x
→(or3
ex3_2
T
nat
λ:T.λj:nat.eq nat i (s k j)
λu2:T.λ:nat.eq C x (CHead c1 k u2)
λu2:T.λj:nat.subst0 j v u1 u2
ex3_2
C
nat
λ:C.λj:nat.eq nat i (s k j)
λc2:C.λ:nat.eq C x (CHead c2 k u1)
λc2:C.λj:nat.csubst0 j v c1 c2
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat i (s k j)
λu2:T.λc2:C.λ:nat.eq C x (CHead c2 k u2)
λu2:T.λ:C.λj:nat.subst0 j v u1 u2
λ:T.λc2:C.λj:nat.csubst0 j v c1 c2)
BODY =
assume k: K
assume c1: C
assume x: C
assume u1: T
assume v: T
assume i: nat
suppose H: csubst0 i v (CHead c1 k u1) x
assume y: C
suppose H0: csubst0 i v y x
we proceed by induction on H0 to prove
eq C y (CHead c1 k u1)
→(or3
ex3_2
T
nat
λ:T.λj:nat.eq nat i (s k j)
λu2:T.λ:nat.eq C x (CHead c1 k u2)
λu2:T.λj:nat.subst0 j v u1 u2
ex3_2
C
nat
λ:C.λj:nat.eq nat i (s k j)
λc2:C.λ:nat.eq C x (CHead c2 k u1)
λc2:C.λj:nat.csubst0 j v c1 c2
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat i (s k j)
λu2:T.λc2:C.λ:nat.eq C x (CHead c2 k u2)
λu2:T.λ:C.λj:nat.subst0 j v u1 u2
λ:T.λc2:C.λj:nat.csubst0 j v c1 c2)
case csubst0_snd : k0:K i0:nat v0:T u0:T u2:T H1:subst0 i0 v0 u0 u2 c:C ⇒
the thesis becomes
∀H2:eq C (CHead c k0 u0) (CHead c1 k u1)
.or3
ex3_2
T
nat
λ:T.λj:nat.eq nat (s k0 i0) (s k j)
λu3:T.λ:nat.eq C (CHead c k0 u2) (CHead c1 k u3)
λu3:T.λj:nat.subst0 j v0 u1 u3
ex3_2
C
nat
λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λc2:C.λ:nat.eq C (CHead c k0 u2) (CHead c2 k u1)
λc2:C.λj:nat.csubst0 j v0 c1 c2
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λu3:T.λc2:C.λ:nat.eq C (CHead c k0 u2) (CHead c2 k u3)
λu3:T.λ:C.λj:nat.subst0 j v0 u1 u3
λ:T.λc2:C.λj:nat.csubst0 j v0 c1 c2
suppose H2: eq C (CHead c k0 u0) (CHead c1 k u1)
(H3)
by (f_equal . . . . . H2)
we proved
eq
C
<λ:C.C> CASE CHead c k0 u0 OF CSort ⇒c | CHead c0 ⇒c0
<λ:C.C> CASE CHead c1 k u1 OF CSort ⇒c | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒c | CHead c0 ⇒c0 (CHead c k0 u0)
λe:C.<λ:C.C> CASE e OF CSort ⇒c | CHead c0 ⇒c0 (CHead c1 k u1)
end of H3
(h1)
(H4)
by (f_equal . . . . . H2)
we proved
eq
K
<λ:C.K> CASE CHead c k0 u0 OF CSort ⇒k0 | CHead k1 ⇒k1
<λ:C.K> CASE CHead c1 k u1 OF CSort ⇒k0 | CHead k1 ⇒k1
eq
K
λe:C.<λ:C.K> CASE e OF CSort ⇒k0 | CHead k1 ⇒k1 (CHead c k0 u0)
λe:C.<λ:C.K> CASE e OF CSort ⇒k0 | CHead k1 ⇒k1 (CHead c1 k u1)
end of H4
(h1)
(H5)
by (f_equal . . . . . H2)
we proved
eq
T
<λ:C.T> CASE CHead c k0 u0 OF CSort ⇒u0 | CHead t⇒t
<λ:C.T> CASE CHead c1 k u1 OF CSort ⇒u0 | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u0 | CHead t⇒t (CHead c k0 u0)
λe:C.<λ:C.T> CASE e OF CSort ⇒u0 | CHead t⇒t (CHead c1 k u1)
end of H5
suppose H6: eq K k0 k
suppose H7: eq C c c1
(H8)
consider H5
we proved
eq
T
<λ:C.T> CASE CHead c k0 u0 OF CSort ⇒u0 | CHead t⇒t
<λ:C.T> CASE CHead c1 k u1 OF CSort ⇒u0 | CHead t⇒t
that is equivalent to eq T u0 u1
we proceed by induction on the previous result to prove subst0 i0 v0 u1 u2
case refl_equal : ⇒
the thesis becomes the hypothesis H1
subst0 i0 v0 u1 u2
end of H8
(h1)
by (refl_equal . .)
eq nat (s k i0) (s k i0)
end of h1
(h2)
by (refl_equal . .)
eq C (CHead c1 k u2) (CHead c1 k u2)
end of h2
by (ex3_2_intro . . . . . . . h1 h2 H8)
we proved
ex3_2
T
nat
λ:T.λj:nat.eq nat (s k i0) (s k j)
λu3:T.λ:nat.eq C (CHead c1 k u2) (CHead c1 k u3)
λu3:T.λj:nat.subst0 j v0 u1 u3
by (or3_intro0 . . . previous)
we proved
or3
ex3_2
T
nat
λ:T.λj:nat.eq nat (s k i0) (s k j)
λu3:T.λ:nat.eq C (CHead c1 k u2) (CHead c1 k u3)
λu3:T.λj:nat.subst0 j v0 u1 u3
ex3_2
C
nat
λ:C.λj:nat.eq nat (s k i0) (s k j)
λc2:C.λ:nat.eq C (CHead c1 k u2) (CHead c2 k u1)
λc2:C.λj:nat.csubst0 j v0 c1 c2
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat (s k i0) (s k j)
λu3:T.λc2:C.λ:nat.eq C (CHead c1 k u2) (CHead c2 k u3)
λu3:T.λ:C.λj:nat.subst0 j v0 u1 u3
λ:T.λc2:C.λj:nat.csubst0 j v0 c1 c2
by (eq_ind_r . . . previous . H6)
we proved
or3
ex3_2
T
nat
λ:T.λj:nat.eq nat (s k0 i0) (s k j)
λu3:T.λ:nat.eq C (CHead c1 k0 u2) (CHead c1 k u3)
λu3:T.λj:nat.subst0 j v0 u1 u3
ex3_2
C
nat
λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λc2:C.λ:nat.eq C (CHead c1 k0 u2) (CHead c2 k u1)
λc2:C.λj:nat.csubst0 j v0 c1 c2
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λu3:T.λc2:C.λ:nat.eq C (CHead c1 k0 u2) (CHead c2 k u3)
λu3:T.λ:C.λj:nat.subst0 j v0 u1 u3
λ:T.λc2:C.λj:nat.csubst0 j v0 c1 c2
by (eq_ind_r . . . previous . H7)
we proved
or3
ex3_2
T
nat
λ:T.λj:nat.eq nat (s k0 i0) (s k j)
λu3:T.λ:nat.eq C (CHead c k0 u2) (CHead c1 k u3)
λu3:T.λj:nat.subst0 j v0 u1 u3
ex3_2
C
nat
λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λc2:C.λ:nat.eq C (CHead c k0 u2) (CHead c2 k u1)
λc2:C.λj:nat.csubst0 j v0 c1 c2
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λu3:T.λc2:C.λ:nat.eq C (CHead c k0 u2) (CHead c2 k u3)
λu3:T.λ:C.λj:nat.subst0 j v0 u1 u3
λ:T.λc2:C.λj:nat.csubst0 j v0 c1 c2
eq K k0 k
→(eq C c c1
→(or3
ex3_2
T
nat
λ:T.λj:nat.eq nat (s k0 i0) (s k j)
λu3:T.λ:nat.eq C (CHead c k0 u2) (CHead c1 k u3)
λu3:T.λj:nat.subst0 j v0 u1 u3
ex3_2
C
nat
λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λc2:C.λ:nat.eq C (CHead c k0 u2) (CHead c2 k u1)
λc2:C.λj:nat.csubst0 j v0 c1 c2
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λu3:T.λc2:C.λ:nat.eq C (CHead c k0 u2) (CHead c2 k u3)
λu3:T.λ:C.λj:nat.subst0 j v0 u1 u3
λ:T.λc2:C.λj:nat.csubst0 j v0 c1 c2))
end of h1
(h2)
consider H4
we proved
eq
K
<λ:C.K> CASE CHead c k0 u0 OF CSort ⇒k0 | CHead k1 ⇒k1
<λ:C.K> CASE CHead c1 k u1 OF CSort ⇒k0 | CHead k1 ⇒k1
eq K k0 k
end of h2
by (h1 h2)
eq C c c1
→(or3
ex3_2
T
nat
λ:T.λj:nat.eq nat (s k0 i0) (s k j)
λu3:T.λ:nat.eq C (CHead c k0 u2) (CHead c1 k u3)
λu3:T.λj:nat.subst0 j v0 u1 u3
ex3_2
C
nat
λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λc2:C.λ:nat.eq C (CHead c k0 u2) (CHead c2 k u1)
λc2:C.λj:nat.csubst0 j v0 c1 c2
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λu3:T.λc2:C.λ:nat.eq C (CHead c k0 u2) (CHead c2 k u3)
λu3:T.λ:C.λj:nat.subst0 j v0 u1 u3
λ:T.λc2:C.λj:nat.csubst0 j v0 c1 c2)
end of h1
(h2)
consider H3
we proved
eq
C
<λ:C.C> CASE CHead c k0 u0 OF CSort ⇒c | CHead c0 ⇒c0
<λ:C.C> CASE CHead c1 k u1 OF CSort ⇒c | CHead c0 ⇒c0
eq C c c1
end of h2
by (h1 h2)
we proved
or3
ex3_2
T
nat
λ:T.λj:nat.eq nat (s k0 i0) (s k j)
λu3:T.λ:nat.eq C (CHead c k0 u2) (CHead c1 k u3)
λu3:T.λj:nat.subst0 j v0 u1 u3
ex3_2
C
nat
λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λc2:C.λ:nat.eq C (CHead c k0 u2) (CHead c2 k u1)
λc2:C.λj:nat.csubst0 j v0 c1 c2
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λu3:T.λc2:C.λ:nat.eq C (CHead c k0 u2) (CHead c2 k u3)
λu3:T.λ:C.λj:nat.subst0 j v0 u1 u3
λ:T.λc2:C.λj:nat.csubst0 j v0 c1 c2
∀H2:eq C (CHead c k0 u0) (CHead c1 k u1)
.or3
ex3_2
T
nat
λ:T.λj:nat.eq nat (s k0 i0) (s k j)
λu3:T.λ:nat.eq C (CHead c k0 u2) (CHead c1 k u3)
λu3:T.λj:nat.subst0 j v0 u1 u3
ex3_2
C
nat
λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λc2:C.λ:nat.eq C (CHead c k0 u2) (CHead c2 k u1)
λc2:C.λj:nat.csubst0 j v0 c1 c2
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λu3:T.λc2:C.λ:nat.eq C (CHead c k0 u2) (CHead c2 k u3)
λu3:T.λ:C.λj:nat.subst0 j v0 u1 u3
λ:T.λc2:C.λj:nat.csubst0 j v0 c1 c2
case csubst0_fst : k0:K i0:nat c0:C c2:C v0:T H1:csubst0 i0 v0 c0 c2 u:T ⇒
the thesis becomes
∀H3:eq C (CHead c0 k0 u) (CHead c1 k u1)
.or3
ex3_2
T
nat
λ:T.λj:nat.eq nat (s k0 i0) (s k j)
λu2:T.λ:nat.eq C (CHead c2 k0 u) (CHead c1 k u2)
λu2:T.λj:nat.subst0 j v0 u1 u2
ex3_2
C
nat
λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λc3:C.λ:nat.eq C (CHead c2 k0 u) (CHead c3 k u1)
λc3:C.λj:nat.csubst0 j v0 c1 c3
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λu2:T.λc3:C.λ:nat.eq C (CHead c2 k0 u) (CHead c3 k u2)
λu2:T.λ:C.λj:nat.subst0 j v0 u1 u2
λ:T.λc3:C.λj:nat.csubst0 j v0 c1 c3
(H2) by induction hypothesis we know
eq C c0 (CHead c1 k u1)
→(or3
ex3_2 T nat λ:T.λj:nat.eq nat i0 (s k j) λu2:T.λ:nat.eq C c2 (CHead c1 k u2) λu2:T.λj:nat.subst0 j v0 u1 u2
ex3_2 C nat λ:C.λj:nat.eq nat i0 (s k j) λc3:C.λ:nat.eq C c2 (CHead c3 k u1) λc3:C.λj:nat.csubst0 j v0 c1 c3
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat i0 (s k j)
λu2:T.λc3:C.λ:nat.eq C c2 (CHead c3 k u2)
λu2:T.λ:C.λj:nat.subst0 j v0 u1 u2
λ:T.λc3:C.λj:nat.csubst0 j v0 c1 c3)
suppose H3: eq C (CHead c0 k0 u) (CHead c1 k u1)
(H4)
by (f_equal . . . . . H3)
we proved
eq
C
<λ:C.C> CASE CHead c0 k0 u OF CSort ⇒c0 | CHead c ⇒c
<λ:C.C> CASE CHead c1 k u1 OF CSort ⇒c0 | CHead c ⇒c
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒c0 | CHead c ⇒c (CHead c0 k0 u)
λe:C.<λ:C.C> CASE e OF CSort ⇒c0 | CHead c ⇒c (CHead c1 k u1)
end of H4
(h1)
(H5)
by (f_equal . . . . . H3)
we proved
eq
K
<λ:C.K> CASE CHead c0 k0 u OF CSort ⇒k0 | CHead k1 ⇒k1
<λ:C.K> CASE CHead c1 k u1 OF CSort ⇒k0 | CHead k1 ⇒k1
eq
K
λe:C.<λ:C.K> CASE e OF CSort ⇒k0 | CHead k1 ⇒k1 (CHead c0 k0 u)
λe:C.<λ:C.K> CASE e OF CSort ⇒k0 | CHead k1 ⇒k1 (CHead c1 k u1)
end of H5
(h1)
(H6)
by (f_equal . . . . . H3)
we proved
eq
T
<λ:C.T> CASE CHead c0 k0 u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead c1 k u1 OF CSort ⇒u | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t (CHead c0 k0 u)
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t (CHead c1 k u1)
end of H6
suppose H7: eq K k0 k
suppose H8: eq C c0 c1
(h1)
(H10)
we proceed by induction on H8 to prove csubst0 i0 v0 c1 c2
case refl_equal : ⇒
the thesis becomes the hypothesis H1
csubst0 i0 v0 c1 c2
end of H10
(h1)
by (refl_equal . .)
eq nat (s k i0) (s k i0)
end of h1
(h2)
by (refl_equal . .)
eq C (CHead c2 k u1) (CHead c2 k u1)
end of h2
by (ex3_2_intro . . . . . . . h1 h2 H10)
we proved
ex3_2
C
nat
λ:C.λj:nat.eq nat (s k i0) (s k j)
λc3:C.λ:nat.eq C (CHead c2 k u1) (CHead c3 k u1)
λc3:C.λj:nat.csubst0 j v0 c1 c3
by (or3_intro1 . . . previous)
we proved
or3
ex3_2
T
nat
λ:T.λj:nat.eq nat (s k i0) (s k j)
λu2:T.λ:nat.eq C (CHead c2 k u1) (CHead c1 k u2)
λu2:T.λj:nat.subst0 j v0 u1 u2
ex3_2
C
nat
λ:C.λj:nat.eq nat (s k i0) (s k j)
λc3:C.λ:nat.eq C (CHead c2 k u1) (CHead c3 k u1)
λc3:C.λj:nat.csubst0 j v0 c1 c3
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat (s k i0) (s k j)
λu2:T.λc3:C.λ:nat.eq C (CHead c2 k u1) (CHead c3 k u2)
λu2:T.λ:C.λj:nat.subst0 j v0 u1 u2
λ:T.λc3:C.λj:nat.csubst0 j v0 c1 c3
by (eq_ind_r . . . previous . H7)
or3
ex3_2
T
nat
λ:T.λj:nat.eq nat (s k0 i0) (s k j)
λu2:T.λ:nat.eq C (CHead c2 k0 u1) (CHead c1 k u2)
λu2:T.λj:nat.subst0 j v0 u1 u2
ex3_2
C
nat
λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λc3:C.λ:nat.eq C (CHead c2 k0 u1) (CHead c3 k u1)
λc3:C.λj:nat.csubst0 j v0 c1 c3
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λu2:T.λc3:C.λ:nat.eq C (CHead c2 k0 u1) (CHead c3 k u2)
λu2:T.λ:C.λj:nat.subst0 j v0 u1 u2
λ:T.λc3:C.λj:nat.csubst0 j v0 c1 c3
end of h1
(h2)
consider H6
we proved
eq
T
<λ:C.T> CASE CHead c0 k0 u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead c1 k u1 OF CSort ⇒u | CHead t⇒t
eq T u u1
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
or3
ex3_2
T
nat
λ:T.λj:nat.eq nat (s k0 i0) (s k j)
λu2:T.λ:nat.eq C (CHead c2 k0 u) (CHead c1 k u2)
λu2:T.λj:nat.subst0 j v0 u1 u2
ex3_2
C
nat
λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λc3:C.λ:nat.eq C (CHead c2 k0 u) (CHead c3 k u1)
λc3:C.λj:nat.csubst0 j v0 c1 c3
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λu2:T.λc3:C.λ:nat.eq C (CHead c2 k0 u) (CHead c3 k u2)
λu2:T.λ:C.λj:nat.subst0 j v0 u1 u2
λ:T.λc3:C.λj:nat.csubst0 j v0 c1 c3
eq K k0 k
→(eq C c0 c1
→(or3
ex3_2
T
nat
λ:T.λj:nat.eq nat (s k0 i0) (s k j)
λu2:T.λ:nat.eq C (CHead c2 k0 u) (CHead c1 k u2)
λu2:T.λj:nat.subst0 j v0 u1 u2
ex3_2
C
nat
λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λc3:C.λ:nat.eq C (CHead c2 k0 u) (CHead c3 k u1)
λc3:C.λj:nat.csubst0 j v0 c1 c3
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λu2:T.λc3:C.λ:nat.eq C (CHead c2 k0 u) (CHead c3 k u2)
λu2:T.λ:C.λj:nat.subst0 j v0 u1 u2
λ:T.λc3:C.λj:nat.csubst0 j v0 c1 c3))
end of h1
(h2)
consider H5
we proved
eq
K
<λ:C.K> CASE CHead c0 k0 u OF CSort ⇒k0 | CHead k1 ⇒k1
<λ:C.K> CASE CHead c1 k u1 OF CSort ⇒k0 | CHead k1 ⇒k1
eq K k0 k
end of h2
by (h1 h2)
eq C c0 c1
→(or3
ex3_2
T
nat
λ:T.λj:nat.eq nat (s k0 i0) (s k j)
λu2:T.λ:nat.eq C (CHead c2 k0 u) (CHead c1 k u2)
λu2:T.λj:nat.subst0 j v0 u1 u2
ex3_2
C
nat
λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λc3:C.λ:nat.eq C (CHead c2 k0 u) (CHead c3 k u1)
λc3:C.λj:nat.csubst0 j v0 c1 c3
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λu2:T.λc3:C.λ:nat.eq C (CHead c2 k0 u) (CHead c3 k u2)
λu2:T.λ:C.λj:nat.subst0 j v0 u1 u2
λ:T.λc3:C.λj:nat.csubst0 j v0 c1 c3)
end of h1
(h2)
consider H4
we proved
eq
C
<λ:C.C> CASE CHead c0 k0 u OF CSort ⇒c0 | CHead c ⇒c
<λ:C.C> CASE CHead c1 k u1 OF CSort ⇒c0 | CHead c ⇒c
eq C c0 c1
end of h2
by (h1 h2)
we proved
or3
ex3_2
T
nat
λ:T.λj:nat.eq nat (s k0 i0) (s k j)
λu2:T.λ:nat.eq C (CHead c2 k0 u) (CHead c1 k u2)
λu2:T.λj:nat.subst0 j v0 u1 u2
ex3_2
C
nat
λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λc3:C.λ:nat.eq C (CHead c2 k0 u) (CHead c3 k u1)
λc3:C.λj:nat.csubst0 j v0 c1 c3
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λu2:T.λc3:C.λ:nat.eq C (CHead c2 k0 u) (CHead c3 k u2)
λu2:T.λ:C.λj:nat.subst0 j v0 u1 u2
λ:T.λc3:C.λj:nat.csubst0 j v0 c1 c3
∀H3:eq C (CHead c0 k0 u) (CHead c1 k u1)
.or3
ex3_2
T
nat
λ:T.λj:nat.eq nat (s k0 i0) (s k j)
λu2:T.λ:nat.eq C (CHead c2 k0 u) (CHead c1 k u2)
λu2:T.λj:nat.subst0 j v0 u1 u2
ex3_2
C
nat
λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λc3:C.λ:nat.eq C (CHead c2 k0 u) (CHead c3 k u1)
λc3:C.λj:nat.csubst0 j v0 c1 c3
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λu2:T.λc3:C.λ:nat.eq C (CHead c2 k0 u) (CHead c3 k u2)
λu2:T.λ:C.λj:nat.subst0 j v0 u1 u2
λ:T.λc3:C.λj:nat.csubst0 j v0 c1 c3
case csubst0_both : k0:K i0:nat v0:T u0:T u2:T H1:subst0 i0 v0 u0 u2 c0:C c2:C H2:csubst0 i0 v0 c0 c2 ⇒
the thesis becomes
∀H4:eq C (CHead c0 k0 u0) (CHead c1 k u1)
.or3
ex3_2
T
nat
λ:T.λj:nat.eq nat (s k0 i0) (s k j)
λu3:T.λ:nat.eq C (CHead c2 k0 u2) (CHead c1 k u3)
λu3:T.λj:nat.subst0 j v0 u1 u3
ex3_2
C
nat
λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λc3:C.λ:nat.eq C (CHead c2 k0 u2) (CHead c3 k u1)
λc3:C.λj:nat.csubst0 j v0 c1 c3
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λu3:T.λc3:C.λ:nat.eq C (CHead c2 k0 u2) (CHead c3 k u3)
λu3:T.λ:C.λj:nat.subst0 j v0 u1 u3
λ:T.λc3:C.λj:nat.csubst0 j v0 c1 c3
(H3) by induction hypothesis we know
eq C c0 (CHead c1 k u1)
→(or3
ex3_2 T nat λ:T.λj:nat.eq nat i0 (s k j) λu3:T.λ:nat.eq C c2 (CHead c1 k u3) λu3:T.λj:nat.subst0 j v0 u1 u3
ex3_2 C nat λ:C.λj:nat.eq nat i0 (s k j) λc3:C.λ:nat.eq C c2 (CHead c3 k u1) λc3:C.λj:nat.csubst0 j v0 c1 c3
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat i0 (s k j)
λu3:T.λc3:C.λ:nat.eq C c2 (CHead c3 k u3)
λu3:T.λ:C.λj:nat.subst0 j v0 u1 u3
λ:T.λc3:C.λj:nat.csubst0 j v0 c1 c3)
suppose H4: eq C (CHead c0 k0 u0) (CHead c1 k u1)
(H5)
by (f_equal . . . . . H4)
we proved
eq
C
<λ:C.C> CASE CHead c0 k0 u0 OF CSort ⇒c0 | CHead c ⇒c
<λ:C.C> CASE CHead c1 k u1 OF CSort ⇒c0 | CHead c ⇒c
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒c0 | CHead c ⇒c (CHead c0 k0 u0)
λe:C.<λ:C.C> CASE e OF CSort ⇒c0 | CHead c ⇒c (CHead c1 k u1)
end of H5
(h1)
(H6)
by (f_equal . . . . . H4)
we proved
eq
K
<λ:C.K> CASE CHead c0 k0 u0 OF CSort ⇒k0 | CHead k1 ⇒k1
<λ:C.K> CASE CHead c1 k u1 OF CSort ⇒k0 | CHead k1 ⇒k1
eq
K
λe:C.<λ:C.K> CASE e OF CSort ⇒k0 | CHead k1 ⇒k1 (CHead c0 k0 u0)
λe:C.<λ:C.K> CASE e OF CSort ⇒k0 | CHead k1 ⇒k1 (CHead c1 k u1)
end of H6
(h1)
(H7)
by (f_equal . . . . . H4)
we proved
eq
T
<λ:C.T> CASE CHead c0 k0 u0 OF CSort ⇒u0 | CHead t⇒t
<λ:C.T> CASE CHead c1 k u1 OF CSort ⇒u0 | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u0 | CHead t⇒t (CHead c0 k0 u0)
λe:C.<λ:C.T> CASE e OF CSort ⇒u0 | CHead t⇒t (CHead c1 k u1)
end of H7
suppose H8: eq K k0 k
suppose H9: eq C c0 c1
(H11)
we proceed by induction on H9 to prove csubst0 i0 v0 c1 c2
case refl_equal : ⇒
the thesis becomes the hypothesis H2
csubst0 i0 v0 c1 c2
end of H11
(H12)
consider H7
we proved
eq
T
<λ:C.T> CASE CHead c0 k0 u0 OF CSort ⇒u0 | CHead t⇒t
<λ:C.T> CASE CHead c1 k u1 OF CSort ⇒u0 | CHead t⇒t
that is equivalent to eq T u0 u1
we proceed by induction on the previous result to prove subst0 i0 v0 u1 u2
case refl_equal : ⇒
the thesis becomes the hypothesis H1
subst0 i0 v0 u1 u2
end of H12
(h1)
by (refl_equal . .)
eq nat (s k i0) (s k i0)
end of h1
(h2)
by (refl_equal . .)
eq C (CHead c2 k u2) (CHead c2 k u2)
end of h2
by (ex4_3_intro . . . . . . . . . . h1 h2 H12 H11)
we proved
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat (s k i0) (s k j)
λu3:T.λc3:C.λ:nat.eq C (CHead c2 k u2) (CHead c3 k u3)
λu3:T.λ:C.λj:nat.subst0 j v0 u1 u3
λ:T.λc3:C.λj:nat.csubst0 j v0 c1 c3
by (or3_intro2 . . . previous)
we proved
or3
ex3_2
T
nat
λ:T.λj:nat.eq nat (s k i0) (s k j)
λu3:T.λ:nat.eq C (CHead c2 k u2) (CHead c1 k u3)
λu3:T.λj:nat.subst0 j v0 u1 u3
ex3_2
C
nat
λ:C.λj:nat.eq nat (s k i0) (s k j)
λc3:C.λ:nat.eq C (CHead c2 k u2) (CHead c3 k u1)
λc3:C.λj:nat.csubst0 j v0 c1 c3
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat (s k i0) (s k j)
λu3:T.λc3:C.λ:nat.eq C (CHead c2 k u2) (CHead c3 k u3)
λu3:T.λ:C.λj:nat.subst0 j v0 u1 u3
λ:T.λc3:C.λj:nat.csubst0 j v0 c1 c3
by (eq_ind_r . . . previous . H8)
we proved
or3
ex3_2
T
nat
λ:T.λj:nat.eq nat (s k0 i0) (s k j)
λu3:T.λ:nat.eq C (CHead c2 k0 u2) (CHead c1 k u3)
λu3:T.λj:nat.subst0 j v0 u1 u3
ex3_2
C
nat
λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λc3:C.λ:nat.eq C (CHead c2 k0 u2) (CHead c3 k u1)
λc3:C.λj:nat.csubst0 j v0 c1 c3
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λu3:T.λc3:C.λ:nat.eq C (CHead c2 k0 u2) (CHead c3 k u3)
λu3:T.λ:C.λj:nat.subst0 j v0 u1 u3
λ:T.λc3:C.λj:nat.csubst0 j v0 c1 c3
eq K k0 k
→(eq C c0 c1
→(or3
ex3_2
T
nat
λ:T.λj:nat.eq nat (s k0 i0) (s k j)
λu3:T.λ:nat.eq C (CHead c2 k0 u2) (CHead c1 k u3)
λu3:T.λj:nat.subst0 j v0 u1 u3
ex3_2
C
nat
λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λc3:C.λ:nat.eq C (CHead c2 k0 u2) (CHead c3 k u1)
λc3:C.λj:nat.csubst0 j v0 c1 c3
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λu3:T.λc3:C.λ:nat.eq C (CHead c2 k0 u2) (CHead c3 k u3)
λu3:T.λ:C.λj:nat.subst0 j v0 u1 u3
λ:T.λc3:C.λj:nat.csubst0 j v0 c1 c3))
end of h1
(h2)
consider H6
we proved
eq
K
<λ:C.K> CASE CHead c0 k0 u0 OF CSort ⇒k0 | CHead k1 ⇒k1
<λ:C.K> CASE CHead c1 k u1 OF CSort ⇒k0 | CHead k1 ⇒k1
eq K k0 k
end of h2
by (h1 h2)
eq C c0 c1
→(or3
ex3_2
T
nat
λ:T.λj:nat.eq nat (s k0 i0) (s k j)
λu3:T.λ:nat.eq C (CHead c2 k0 u2) (CHead c1 k u3)
λu3:T.λj:nat.subst0 j v0 u1 u3
ex3_2
C
nat
λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λc3:C.λ:nat.eq C (CHead c2 k0 u2) (CHead c3 k u1)
λc3:C.λj:nat.csubst0 j v0 c1 c3
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λu3:T.λc3:C.λ:nat.eq C (CHead c2 k0 u2) (CHead c3 k u3)
λu3:T.λ:C.λj:nat.subst0 j v0 u1 u3
λ:T.λc3:C.λj:nat.csubst0 j v0 c1 c3)
end of h1
(h2)
consider H5
we proved
eq
C
<λ:C.C> CASE CHead c0 k0 u0 OF CSort ⇒c0 | CHead c ⇒c
<λ:C.C> CASE CHead c1 k u1 OF CSort ⇒c0 | CHead c ⇒c
eq C c0 c1
end of h2
by (h1 h2)
we proved
or3
ex3_2
T
nat
λ:T.λj:nat.eq nat (s k0 i0) (s k j)
λu3:T.λ:nat.eq C (CHead c2 k0 u2) (CHead c1 k u3)
λu3:T.λj:nat.subst0 j v0 u1 u3
ex3_2
C
nat
λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λc3:C.λ:nat.eq C (CHead c2 k0 u2) (CHead c3 k u1)
λc3:C.λj:nat.csubst0 j v0 c1 c3
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λu3:T.λc3:C.λ:nat.eq C (CHead c2 k0 u2) (CHead c3 k u3)
λu3:T.λ:C.λj:nat.subst0 j v0 u1 u3
λ:T.λc3:C.λj:nat.csubst0 j v0 c1 c3
∀H4:eq C (CHead c0 k0 u0) (CHead c1 k u1)
.or3
ex3_2
T
nat
λ:T.λj:nat.eq nat (s k0 i0) (s k j)
λu3:T.λ:nat.eq C (CHead c2 k0 u2) (CHead c1 k u3)
λu3:T.λj:nat.subst0 j v0 u1 u3
ex3_2
C
nat
λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λc3:C.λ:nat.eq C (CHead c2 k0 u2) (CHead c3 k u1)
λc3:C.λj:nat.csubst0 j v0 c1 c3
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat (s k0 i0) (s k j)
λu3:T.λc3:C.λ:nat.eq C (CHead c2 k0 u2) (CHead c3 k u3)
λu3:T.λ:C.λj:nat.subst0 j v0 u1 u3
λ:T.λc3:C.λj:nat.csubst0 j v0 c1 c3
we proved
eq C y (CHead c1 k u1)
→(or3
ex3_2
T
nat
λ:T.λj:nat.eq nat i (s k j)
λu2:T.λ:nat.eq C x (CHead c1 k u2)
λu2:T.λj:nat.subst0 j v u1 u2
ex3_2
C
nat
λ:C.λj:nat.eq nat i (s k j)
λc2:C.λ:nat.eq C x (CHead c2 k u1)
λc2:C.λj:nat.csubst0 j v c1 c2
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat i (s k j)
λu2:T.λc2:C.λ:nat.eq C x (CHead c2 k u2)
λu2:T.λ:C.λj:nat.subst0 j v u1 u2
λ:T.λc2:C.λj:nat.csubst0 j v c1 c2)
we proved
∀y:C
.csubst0 i v y x
→(eq C y (CHead c1 k u1)
→(or3
ex3_2
T
nat
λ:T.λj:nat.eq nat i (s k j)
λu2:T.λ:nat.eq C x (CHead c1 k u2)
λu2:T.λj:nat.subst0 j v u1 u2
ex3_2
C
nat
λ:C.λj:nat.eq nat i (s k j)
λc2:C.λ:nat.eq C x (CHead c2 k u1)
λc2:C.λj:nat.csubst0 j v c1 c2
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat i (s k j)
λu2:T.λc2:C.λ:nat.eq C x (CHead c2 k u2)
λu2:T.λ:C.λj:nat.subst0 j v u1 u2
λ:T.λc2:C.λj:nat.csubst0 j v c1 c2))
by (insert_eq . . . . previous H)
we proved
or3
ex3_2
T
nat
λ:T.λj:nat.eq nat i (s k j)
λu2:T.λ:nat.eq C x (CHead c1 k u2)
λu2:T.λj:nat.subst0 j v u1 u2
ex3_2
C
nat
λ:C.λj:nat.eq nat i (s k j)
λc2:C.λ:nat.eq C x (CHead c2 k u1)
λc2:C.λj:nat.csubst0 j v c1 c2
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat i (s k j)
λu2:T.λc2:C.λ:nat.eq C x (CHead c2 k u2)
λu2:T.λ:C.λj:nat.subst0 j v u1 u2
λ:T.λc2:C.λj:nat.csubst0 j v c1 c2
we proved
∀k:K
.∀c1:C
.∀x:C
.∀u1:T
.∀v:T
.∀i:nat
.csubst0 i v (CHead c1 k u1) x
→(or3
ex3_2
T
nat
λ:T.λj:nat.eq nat i (s k j)
λu2:T.λ:nat.eq C x (CHead c1 k u2)
λu2:T.λj:nat.subst0 j v u1 u2
ex3_2
C
nat
λ:C.λj:nat.eq nat i (s k j)
λc2:C.λ:nat.eq C x (CHead c2 k u1)
λc2:C.λj:nat.csubst0 j v c1 c2
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat i (s k j)
λu2:T.λc2:C.λ:nat.eq C x (CHead c2 k u2)
λu2:T.λ:C.λj:nat.subst0 j v u1 u2
λ:T.λc2:C.λj:nat.csubst0 j v c1 c2)