DEFINITION csubst1_gen_head()
TYPE =
∀k:K
.∀c1:C
.∀x:C
.∀u1:T
.∀v:T
.∀i:nat
.csubst1 (s k i) v (CHead c1 k u1) x
→ex3_2 T C λu2:T.λc2:C.eq C x (CHead c2 k u2) λu2:T.λ:C.subst1 i v u1 u2 λ:T.λc2:C.csubst1 i v c1 c2
BODY =
assume k: K
assume c1: C
assume x: C
assume u1: T
assume v: T
assume i: nat
suppose H: csubst1 (s k i) v (CHead c1 k u1) x
we proceed by induction on H to prove ex3_2 T C λu2:T.λc2:C.eq C x (CHead c2 k u2) λu2:T.λ:C.subst1 i v u1 u2 λ:T.λc2:C.csubst1 i v c1 c2
case csubst1_refl : ⇒
the thesis becomes ex3_2 T C λu2:T.λc2:C.eq C (CHead c1 k u1) (CHead c2 k u2) λu2:T.λ:C.subst1 i v u1 u2 λ:T.λc2:C.csubst1 i v c1 c2
(h1)
by (refl_equal . .)
eq C (CHead c1 k u1) (CHead c1 k u1)
end of h1
(h2)
by (subst1_refl . . .)
subst1 i v u1 u1
end of h2
(h3)
by (csubst1_refl . . .)
csubst1 i v c1 c1
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
ex3_2 T C λu2:T.λc2:C.eq C (CHead c1 k u1) (CHead c2 k u2) λu2:T.λ:C.subst1 i v u1 u2 λ:T.λc2:C.csubst1 i v c1 c2
case csubst1_sing : c2:C H0:csubst0 (s k i) v (CHead c1 k u1) c2 ⇒
the thesis becomes ex3_2 T C λu2:T.λc3:C.eq C c2 (CHead c3 k u2) λu2:T.λ:C.subst1 i v u1 u2 λ:T.λc3:C.csubst1 i v c1 c3
by (csubst0_gen_head . . . . . . H0)
we proved
or3
ex3_2
T
nat
λ:T.λj:nat.eq nat (s k i) (s k j)
λu2:T.λ:nat.eq C c2 (CHead c1 k u2)
λu2:T.λj:nat.subst0 j v u1 u2
ex3_2
C
nat
λ:C.λj:nat.eq nat (s k i) (s k j)
λc2:C.λ:nat.eq C c2 (CHead c2 k u1)
λc2:C.λj:nat.csubst0 j v c1 c2
ex4_3
T
C
nat
λ:T.λ:C.λj:nat.eq nat (s k i) (s k j)
λu2:T.λc2:C.λ:nat.eq C c2 (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 proceed by induction on the previous result to prove ex3_2 T C λu2:T.λc3:C.eq C c2 (CHead c3 k u2) λu2:T.λ:C.subst1 i v u1 u2 λ:T.λc3:C.csubst1 i v c1 c3
case or3_intro0 : H1:ex3_2 T nat λ:T.λj:nat.eq nat (s k i) (s k j) λu2:T.λ:nat.eq C c2 (CHead c1 k u2) λu2:T.λj:nat.subst0 j v u1 u2 ⇒
the thesis becomes ex3_2 T C λu2:T.λc3:C.eq C c2 (CHead c3 k u2) λu2:T.λ:C.subst1 i v u1 u2 λ:T.λc3:C.csubst1 i v c1 c3
we proceed by induction on H1 to prove ex3_2 T C λu2:T.λc3:C.eq C c2 (CHead c3 k u2) λu2:T.λ:C.subst1 i v u1 u2 λ:T.λc3:C.csubst1 i v c1 c3
case ex3_2_intro : x0:T x1:nat H2:eq nat (s k i) (s k x1) H3:eq C c2 (CHead c1 k x0) H4:subst0 x1 v u1 x0 ⇒
the thesis becomes ex3_2 T C λu2:T.λc3:C.eq C c2 (CHead c3 k u2) λu2:T.λ:C.subst1 i v u1 u2 λ:T.λc3:C.csubst1 i v c1 c3
(H5)
by (s_inj . . . H2)
we proved eq nat i x1
by (eq_ind_r . . . H4 . previous)
subst0 i v u1 x0
end of H5
(h1)
by (refl_equal . .)
eq C (CHead c1 k x0) (CHead c1 k x0)
end of h1
(h2)
by (subst1_single . . . . H5)
subst1 i v u1 x0
end of h2
(h3)
by (csubst1_refl . . .)
csubst1 i v c1 c1
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
we proved ex3_2 T C λu2:T.λc3:C.eq C (CHead c1 k x0) (CHead c3 k u2) λu2:T.λ:C.subst1 i v u1 u2 λ:T.λc3:C.csubst1 i v c1 c3
by (eq_ind_r . . . previous . H3)
ex3_2 T C λu2:T.λc3:C.eq C c2 (CHead c3 k u2) λu2:T.λ:C.subst1 i v u1 u2 λ:T.λc3:C.csubst1 i v c1 c3
ex3_2 T C λu2:T.λc3:C.eq C c2 (CHead c3 k u2) λu2:T.λ:C.subst1 i v u1 u2 λ:T.λc3:C.csubst1 i v c1 c3
case or3_intro1 : H1:ex3_2 C nat λ:C.λj:nat.eq nat (s k i) (s k j) λc3:C.λ:nat.eq C c2 (CHead c3 k u1) λc3:C.λj:nat.csubst0 j v c1 c3 ⇒
the thesis becomes ex3_2 T C λu2:T.λc3:C.eq C c2 (CHead c3 k u2) λu2:T.λ:C.subst1 i v u1 u2 λ:T.λc3:C.csubst1 i v c1 c3
we proceed by induction on H1 to prove ex3_2 T C λu2:T.λc3:C.eq C c2 (CHead c3 k u2) λu2:T.λ:C.subst1 i v u1 u2 λ:T.λc3:C.csubst1 i v c1 c3
case ex3_2_intro : x0:C x1:nat H2:eq nat (s k i) (s k x1) H3:eq C c2 (CHead x0 k u1) H4:csubst0 x1 v c1 x0 ⇒
the thesis becomes ex3_2 T C λu2:T.λc3:C.eq C c2 (CHead c3 k u2) λu2:T.λ:C.subst1 i v u1 u2 λ:T.λc3:C.csubst1 i v c1 c3
(H5)
by (s_inj . . . H2)
we proved eq nat i x1
by (eq_ind_r . . . H4 . previous)
csubst0 i v c1 x0
end of H5
(h1)
by (refl_equal . .)
eq C (CHead x0 k u1) (CHead x0 k u1)
end of h1
(h2)
by (subst1_refl . . .)
subst1 i v u1 u1
end of h2
(h3)
by (csubst1_sing . . . . H5)
csubst1 i v c1 x0
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
we proved ex3_2 T C λu2:T.λc3:C.eq C (CHead x0 k u1) (CHead c3 k u2) λu2:T.λ:C.subst1 i v u1 u2 λ:T.λc3:C.csubst1 i v c1 c3
by (eq_ind_r . . . previous . H3)
ex3_2 T C λu2:T.λc3:C.eq C c2 (CHead c3 k u2) λu2:T.λ:C.subst1 i v u1 u2 λ:T.λc3:C.csubst1 i v c1 c3
ex3_2 T C λu2:T.λc3:C.eq C c2 (CHead c3 k u2) λu2:T.λ:C.subst1 i v u1 u2 λ:T.λc3:C.csubst1 i v c1 c3
case or3_intro2 : H1:ex4_3 T C nat λ:T.λ:C.λj:nat.eq nat (s k i) (s k j) λu2:T.λc3:C.λ:nat.eq C c2 (CHead c3 k u2) λu2:T.λ:C.λj:nat.subst0 j v u1 u2 λ:T.λc3:C.λj:nat.csubst0 j v c1 c3 ⇒
the thesis becomes ex3_2 T C λu2:T.λc3:C.eq C c2 (CHead c3 k u2) λu2:T.λ:C.subst1 i v u1 u2 λ:T.λc3:C.csubst1 i v c1 c3
we proceed by induction on H1 to prove ex3_2 T C λu2:T.λc3:C.eq C c2 (CHead c3 k u2) λu2:T.λ:C.subst1 i v u1 u2 λ:T.λc3:C.csubst1 i v c1 c3
case ex4_3_intro : x0:T x1:C x2:nat H2:eq nat (s k i) (s k x2) H3:eq C c2 (CHead x1 k x0) H4:subst0 x2 v u1 x0 H5:csubst0 x2 v c1 x1 ⇒
the thesis becomes ex3_2 T C λu2:T.λc3:C.eq C c2 (CHead c3 k u2) λu2:T.λ:C.subst1 i v u1 u2 λ:T.λc3:C.csubst1 i v c1 c3
(H6)
by (s_inj . . . H2)
we proved eq nat i x2
by (eq_ind_r . . . H5 . previous)
csubst0 i v c1 x1
end of H6
(H7)
by (s_inj . . . H2)
we proved eq nat i x2
by (eq_ind_r . . . H4 . previous)
subst0 i v u1 x0
end of H7
(h1)
by (refl_equal . .)
eq C (CHead x1 k x0) (CHead x1 k x0)
end of h1
(h2)
by (subst1_single . . . . H7)
subst1 i v u1 x0
end of h2
(h3)
by (csubst1_sing . . . . H6)
csubst1 i v c1 x1
end of h3
by (ex3_2_intro . . . . . . . h1 h2 h3)
we proved ex3_2 T C λu2:T.λc3:C.eq C (CHead x1 k x0) (CHead c3 k u2) λu2:T.λ:C.subst1 i v u1 u2 λ:T.λc3:C.csubst1 i v c1 c3
by (eq_ind_r . . . previous . H3)
ex3_2 T C λu2:T.λc3:C.eq C c2 (CHead c3 k u2) λu2:T.λ:C.subst1 i v u1 u2 λ:T.λc3:C.csubst1 i v c1 c3
ex3_2 T C λu2:T.λc3:C.eq C c2 (CHead c3 k u2) λu2:T.λ:C.subst1 i v u1 u2 λ:T.λc3:C.csubst1 i v c1 c3
ex3_2 T C λu2:T.λc3:C.eq C c2 (CHead c3 k u2) λu2:T.λ:C.subst1 i v u1 u2 λ:T.λc3:C.csubst1 i v c1 c3
we proved ex3_2 T C λu2:T.λc2:C.eq C x (CHead c2 k u2) λu2:T.λ:C.subst1 i v u1 u2 λ:T.λc2:C.csubst1 i v c1 c2
we proved
∀k:K
.∀c1:C
.∀x:C
.∀u1:T
.∀v:T
.∀i:nat
.csubst1 (s k i) v (CHead c1 k u1) x
→ex3_2 T C λu2:T.λc2:C.eq C x (CHead c2 k u2) λu2:T.λ:C.subst1 i v u1 u2 λ:T.λc2:C.csubst1 i v c1 c2