DEFINITION subst0_gen_head()
TYPE =
∀k:K
.∀v:T
.∀u1:T
.∀t1:T
.∀x:T
.∀i:nat
.subst0 i v (THead k u1 t1) x
→(or3
ex2 T λu2:T.eq T x (THead k u2 t1) λu2:T.subst0 i v u1 u2
ex2 T λt2:T.eq T x (THead k u1 t2) λt2:T.subst0 (s k i) v t1 t2
ex3_2 T T λu2:T.λt2:T.eq T x (THead k u2 t2) λu2:T.λ:T.subst0 i v u1 u2 λ:T.λt2:T.subst0 (s k i) v t1 t2)
BODY =
assume k: K
assume v: T
assume u1: T
assume t1: T
assume x: T
assume i: nat
suppose H: subst0 i v (THead k u1 t1) x
assume y: T
suppose H0: subst0 i v y x
we proceed by induction on H0 to prove
eq T y (THead k u1 t1)
→(or3
ex2 T λu2:T.eq T x (THead k u2 t1) λu2:T.subst0 i v u1 u2
ex2 T λt3:T.eq T x (THead k u1 t3) λt3:T.subst0 (s k i) v t1 t3
ex3_2 T T λu2:T.λt3:T.eq T x (THead k u2 t3) λu2:T.λ:T.subst0 i v u1 u2 λ:T.λt3:T.subst0 (s k i) v t1 t3)
case subst0_lref : v0:T i0:nat ⇒
the thesis becomes
∀H1:eq T (TLRef i0) (THead k u1 t1)
.or3
ex2 T λu2:T.eq T (lift (S i0) O v0) (THead k u2 t1) λu2:T.subst0 i0 v0 u1 u2
ex2 T λt2:T.eq T (lift (S i0) O v0) (THead k u1 t2) λt2:T.subst0 (s k i0) v0 t1 t2
ex3_2 T T λu2:T.λt2:T.eq T (lift (S i0) O v0) (THead k u2 t2) λu2:T.λ:T.subst0 i0 v0 u1 u2 λ:T.λt2:T.subst0 (s k i0) v0 t1 t2
suppose H1: eq T (TLRef i0) (THead k u1 t1)
(H2)
we proceed by induction on H1 to prove
<λ:T.Prop>
CASE THead k u1 t1 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TLRef i0 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TLRef i0 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
<λ:T.Prop>
CASE THead k u1 t1 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
end of H2
consider H2
we proved
<λ:T.Prop>
CASE THead k u1 t1 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
or3
ex2 T λu2:T.eq T (lift (S i0) O v0) (THead k u2 t1) λu2:T.subst0 i0 v0 u1 u2
ex2 T λt2:T.eq T (lift (S i0) O v0) (THead k u1 t2) λt2:T.subst0 (s k i0) v0 t1 t2
ex3_2 T T λu2:T.λt2:T.eq T (lift (S i0) O v0) (THead k u2 t2) λu2:T.λ:T.subst0 i0 v0 u1 u2 λ:T.λt2:T.subst0 (s k i0) v0 t1 t2
we proved
or3
ex2 T λu2:T.eq T (lift (S i0) O v0) (THead k u2 t1) λu2:T.subst0 i0 v0 u1 u2
ex2 T λt2:T.eq T (lift (S i0) O v0) (THead k u1 t2) λt2:T.subst0 (s k i0) v0 t1 t2
ex3_2 T T λu2:T.λt2:T.eq T (lift (S i0) O v0) (THead k u2 t2) λu2:T.λ:T.subst0 i0 v0 u1 u2 λ:T.λt2:T.subst0 (s k i0) v0 t1 t2
∀H1:eq T (TLRef i0) (THead k u1 t1)
.or3
ex2 T λu2:T.eq T (lift (S i0) O v0) (THead k u2 t1) λu2:T.subst0 i0 v0 u1 u2
ex2 T λt2:T.eq T (lift (S i0) O v0) (THead k u1 t2) λt2:T.subst0 (s k i0) v0 t1 t2
ex3_2 T T λu2:T.λt2:T.eq T (lift (S i0) O v0) (THead k u2 t2) λu2:T.λ:T.subst0 i0 v0 u1 u2 λ:T.λt2:T.subst0 (s k i0) v0 t1 t2
case subst0_fst : v0:T u2:T u0:T i0:nat H1:subst0 i0 v0 u0 u2 t:T k0:K ⇒
the thesis becomes
∀H3:eq T (THead k0 u0 t) (THead k u1 t1)
.or3
ex2 T λu3:T.eq T (THead k0 u2 t) (THead k u3 t1) λu3:T.subst0 i0 v0 u1 u3
ex2 T λt2:T.eq T (THead k0 u2 t) (THead k u1 t2) λt2:T.subst0 (s k i0) v0 t1 t2
ex3_2 T T λu3:T.λt2:T.eq T (THead k0 u2 t) (THead k u3 t2) λu3:T.λ:T.subst0 i0 v0 u1 u3 λ:T.λt2:T.subst0 (s k i0) v0 t1 t2
(H2) by induction hypothesis we know
eq T u0 (THead k u1 t1)
→(or3
ex2 T λu3:T.eq T u2 (THead k u3 t1) λu3:T.subst0 i0 v0 u1 u3
ex2 T λt2:T.eq T u2 (THead k u1 t2) λt2:T.subst0 (s k i0) v0 t1 t2
ex3_2 T T λu3:T.λt2:T.eq T u2 (THead k u3 t2) λu3:T.λ:T.subst0 i0 v0 u1 u3 λ:T.λt2:T.subst0 (s k i0) v0 t1 t2)
suppose H3: eq T (THead k0 u0 t) (THead k u1 t1)
(H4)
by (f_equal . . . . . H3)
we proved
eq
K
<λ:T.K> CASE THead k0 u0 t OF TSort ⇒k0 | TLRef ⇒k0 | THead k1 ⇒k1
<λ:T.K> CASE THead k u1 t1 OF TSort ⇒k0 | TLRef ⇒k0 | THead k1 ⇒k1
eq
K
λe:T.<λ:T.K> CASE e OF TSort ⇒k0 | TLRef ⇒k0 | THead k1 ⇒k1 (THead k0 u0 t)
λe:T.<λ:T.K> CASE e OF TSort ⇒k0 | TLRef ⇒k0 | THead k1 ⇒k1 (THead k u1 t1)
end of H4
(h1)
(H5)
by (f_equal . . . . . H3)
we proved
eq
T
<λ:T.T> CASE THead k0 u0 t OF TSort ⇒u0 | TLRef ⇒u0 | THead t0 ⇒t0
<λ:T.T> CASE THead k u1 t1 OF TSort ⇒u0 | TLRef ⇒u0 | THead t0 ⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒u0 | TLRef ⇒u0 | THead t0 ⇒t0 (THead k0 u0 t)
λe:T.<λ:T.T> CASE e OF TSort ⇒u0 | TLRef ⇒u0 | THead t0 ⇒t0 (THead k u1 t1)
end of H5
(h1)
(H6)
by (f_equal . . . . . H3)
we proved
eq
T
<λ:T.T> CASE THead k0 u0 t OF TSort ⇒t | TLRef ⇒t | THead t0⇒t0
<λ:T.T> CASE THead k u1 t1 OF TSort ⇒t | TLRef ⇒t | THead t0⇒t0
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t | TLRef ⇒t | THead t0⇒t0 (THead k0 u0 t)
λe:T.<λ:T.T> CASE e OF TSort ⇒t | TLRef ⇒t | THead t0⇒t0 (THead k u1 t1)
end of H6
suppose H7: eq T u0 u1
suppose H8: eq K k0 k
(h1)
(H10)
we proceed by induction on H7 to prove subst0 i0 v0 u1 u2
case refl_equal : ⇒
the thesis becomes the hypothesis H1
subst0 i0 v0 u1 u2
end of H10
by (refl_equal . .)
we proved eq T (THead k u2 t1) (THead k u2 t1)
by (ex_intro2 . . . . previous H10)
we proved ex2 T λu3:T.eq T (THead k u2 t1) (THead k u3 t1) λu3:T.subst0 i0 v0 u1 u3
by (or3_intro0 . . . previous)
or3
ex2 T λu3:T.eq T (THead k u2 t1) (THead k u3 t1) λu3:T.subst0 i0 v0 u1 u3
ex2 T λt2:T.eq T (THead k u2 t1) (THead k u1 t2) λt2:T.subst0 (s k i0) v0 t1 t2
ex3_2 T T λu3:T.λt2:T.eq T (THead k u2 t1) (THead k u3 t2) λu3:T.λ:T.subst0 i0 v0 u1 u3 λ:T.λt2:T.subst0 (s k i0) v0 t1 t2
end of h1
(h2)
consider H6
we proved
eq
T
<λ:T.T> CASE THead k0 u0 t OF TSort ⇒t | TLRef ⇒t | THead t0⇒t0
<λ:T.T> CASE THead k u1 t1 OF TSort ⇒t | TLRef ⇒t | THead t0⇒t0
eq T t t1
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
or3
ex2 T λu3:T.eq T (THead k u2 t) (THead k u3 t1) λu3:T.subst0 i0 v0 u1 u3
ex2 T λt2:T.eq T (THead k u2 t) (THead k u1 t2) λt2:T.subst0 (s k i0) v0 t1 t2
ex3_2 T T λu3:T.λt2:T.eq T (THead k u2 t) (THead k u3 t2) λu3:T.λ:T.subst0 i0 v0 u1 u3 λ:T.λt2:T.subst0 (s k i0) v0 t1 t2
by (eq_ind_r . . . previous . H8)
we proved
or3
ex2 T λu3:T.eq T (THead k0 u2 t) (THead k u3 t1) λu3:T.subst0 i0 v0 u1 u3
ex2 T λt2:T.eq T (THead k0 u2 t) (THead k u1 t2) λt2:T.subst0 (s k i0) v0 t1 t2
ex3_2 T T λu3:T.λt2:T.eq T (THead k0 u2 t) (THead k u3 t2) λu3:T.λ:T.subst0 i0 v0 u1 u3 λ:T.λt2:T.subst0 (s k i0) v0 t1 t2
eq T u0 u1
→(eq K k0 k
→(or3
ex2 T λu3:T.eq T (THead k0 u2 t) (THead k u3 t1) λu3:T.subst0 i0 v0 u1 u3
ex2 T λt2:T.eq T (THead k0 u2 t) (THead k u1 t2) λt2:T.subst0 (s k i0) v0 t1 t2
ex3_2 T T λu3:T.λt2:T.eq T (THead k0 u2 t) (THead k u3 t2) λu3:T.λ:T.subst0 i0 v0 u1 u3 λ:T.λt2:T.subst0 (s k i0) v0 t1 t2))
end of h1
(h2)
consider H5
we proved
eq
T
<λ:T.T> CASE THead k0 u0 t OF TSort ⇒u0 | TLRef ⇒u0 | THead t0 ⇒t0
<λ:T.T> CASE THead k u1 t1 OF TSort ⇒u0 | TLRef ⇒u0 | THead t0 ⇒t0
eq T u0 u1
end of h2
by (h1 h2)
eq K k0 k
→(or3
ex2 T λu3:T.eq T (THead k0 u2 t) (THead k u3 t1) λu3:T.subst0 i0 v0 u1 u3
ex2 T λt2:T.eq T (THead k0 u2 t) (THead k u1 t2) λt2:T.subst0 (s k i0) v0 t1 t2
ex3_2 T T λu3:T.λt2:T.eq T (THead k0 u2 t) (THead k u3 t2) λu3:T.λ:T.subst0 i0 v0 u1 u3 λ:T.λt2:T.subst0 (s k i0) v0 t1 t2)
end of h1
(h2)
consider H4
we proved
eq
K
<λ:T.K> CASE THead k0 u0 t OF TSort ⇒k0 | TLRef ⇒k0 | THead k1 ⇒k1
<λ:T.K> CASE THead k u1 t1 OF TSort ⇒k0 | TLRef ⇒k0 | THead k1 ⇒k1
eq K k0 k
end of h2
by (h1 h2)
we proved
or3
ex2 T λu3:T.eq T (THead k0 u2 t) (THead k u3 t1) λu3:T.subst0 i0 v0 u1 u3
ex2 T λt2:T.eq T (THead k0 u2 t) (THead k u1 t2) λt2:T.subst0 (s k i0) v0 t1 t2
ex3_2 T T λu3:T.λt2:T.eq T (THead k0 u2 t) (THead k u3 t2) λu3:T.λ:T.subst0 i0 v0 u1 u3 λ:T.λt2:T.subst0 (s k i0) v0 t1 t2
∀H3:eq T (THead k0 u0 t) (THead k u1 t1)
.or3
ex2 T λu3:T.eq T (THead k0 u2 t) (THead k u3 t1) λu3:T.subst0 i0 v0 u1 u3
ex2 T λt2:T.eq T (THead k0 u2 t) (THead k u1 t2) λt2:T.subst0 (s k i0) v0 t1 t2
ex3_2 T T λu3:T.λt2:T.eq T (THead k0 u2 t) (THead k u3 t2) λu3:T.λ:T.subst0 i0 v0 u1 u3 λ:T.λt2:T.subst0 (s k i0) v0 t1 t2
case subst0_snd : k0:K v0:T t2:T t0:T i0:nat H1:subst0 (s k0 i0) v0 t0 t2 u:T ⇒
the thesis becomes
∀H3:eq T (THead k0 u t0) (THead k u1 t1)
.or3
ex2 T λu2:T.eq T (THead k0 u t2) (THead k u2 t1) λu2:T.subst0 i0 v0 u1 u2
ex2 T λt3:T.eq T (THead k0 u t2) (THead k u1 t3) λt3:T.subst0 (s k i0) v0 t1 t3
ex3_2 T T λu2:T.λt3:T.eq T (THead k0 u t2) (THead k u2 t3) λu2:T.λ:T.subst0 i0 v0 u1 u2 λ:T.λt3:T.subst0 (s k i0) v0 t1 t3
(H2) by induction hypothesis we know
eq T t0 (THead k u1 t1)
→(or3
ex2 T λu2:T.eq T t2 (THead k u2 t1) λu2:T.subst0 (s k0 i0) v0 u1 u2
ex2 T λt3:T.eq T t2 (THead k u1 t3) λt3:T.subst0 (s k (s k0 i0)) v0 t1 t3
ex3_2 T T λu2:T.λt3:T.eq T t2 (THead k u2 t3) λu2:T.λ:T.subst0 (s k0 i0) v0 u1 u2 λ:T.λt3:T.subst0 (s k (s k0 i0)) v0 t1 t3)
suppose H3: eq T (THead k0 u t0) (THead k u1 t1)
(H4)
by (f_equal . . . . . H3)
we proved
eq
K
<λ:T.K> CASE THead k0 u t0 OF TSort ⇒k0 | TLRef ⇒k0 | THead k1 ⇒k1
<λ:T.K> CASE THead k u1 t1 OF TSort ⇒k0 | TLRef ⇒k0 | THead k1 ⇒k1
eq
K
λe:T.<λ:T.K> CASE e OF TSort ⇒k0 | TLRef ⇒k0 | THead k1 ⇒k1 (THead k0 u t0)
λe:T.<λ:T.K> CASE e OF TSort ⇒k0 | TLRef ⇒k0 | THead k1 ⇒k1 (THead k u1 t1)
end of H4
(h1)
(H5)
by (f_equal . . . . . H3)
we proved
eq
T
<λ:T.T> CASE THead k0 u t0 OF TSort ⇒u | TLRef ⇒u | THead t ⇒t
<λ:T.T> CASE THead k u1 t1 OF TSort ⇒u | TLRef ⇒u | THead t ⇒t
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒u | TLRef ⇒u | THead t ⇒t (THead k0 u t0)
λe:T.<λ:T.T> CASE e OF TSort ⇒u | TLRef ⇒u | THead t ⇒t (THead k u1 t1)
end of H5
(h1)
(H6)
by (f_equal . . . . . H3)
we proved
eq
T
<λ:T.T> CASE THead k0 u t0 OF TSort ⇒t0 | TLRef ⇒t0 | THead t⇒t
<λ:T.T> CASE THead k u1 t1 OF TSort ⇒t0 | TLRef ⇒t0 | THead t⇒t
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t0 | TLRef ⇒t0 | THead t⇒t (THead k0 u t0)
λe:T.<λ:T.T> CASE e OF TSort ⇒t0 | TLRef ⇒t0 | THead t⇒t (THead k u1 t1)
end of H6
suppose H7: eq T u u1
suppose H8: eq K k0 k
(H9)
consider H6
we proved
eq
T
<λ:T.T> CASE THead k0 u t0 OF TSort ⇒t0 | TLRef ⇒t0 | THead t⇒t
<λ:T.T> CASE THead k u1 t1 OF TSort ⇒t0 | TLRef ⇒t0 | THead t⇒t
that is equivalent to eq T t0 t1
we proceed by induction on the previous result to prove
eq T t1 (THead k u1 t1)
→(or3
ex2 T λu2:T.eq T t2 (THead k u2 t1) λu2:T.subst0 (s k0 i0) v0 u1 u2
ex2 T λt3:T.eq T t2 (THead k u1 t3) λt3:T.subst0 (s k (s k0 i0)) v0 t1 t3
ex3_2 T T λu2:T.λt3:T.eq T t2 (THead k u2 t3) λu2:T.λ:T.subst0 (s k0 i0) v0 u1 u2 λ:T.λt3:T.subst0 (s k (s k0 i0)) v0 t1 t3)
case refl_equal : ⇒
the thesis becomes the hypothesis H2
eq T t1 (THead k u1 t1)
→(or3
ex2 T λu2:T.eq T t2 (THead k u2 t1) λu2:T.subst0 (s k0 i0) v0 u1 u2
ex2 T λt3:T.eq T t2 (THead k u1 t3) λt3:T.subst0 (s k (s k0 i0)) v0 t1 t3
ex3_2 T T λu2:T.λt3:T.eq T t2 (THead k u2 t3) λu2:T.λ:T.subst0 (s k0 i0) v0 u1 u2 λ:T.λt3:T.subst0 (s k (s k0 i0)) v0 t1 t3)
end of H9
(H10)
consider H6
we proved
eq
T
<λ:T.T> CASE THead k0 u t0 OF TSort ⇒t0 | TLRef ⇒t0 | THead t⇒t
<λ:T.T> CASE THead k u1 t1 OF TSort ⇒t0 | TLRef ⇒t0 | THead t⇒t
that is equivalent to eq T t0 t1
we proceed by induction on the previous result to prove subst0 (s k0 i0) v0 t1 t2
case refl_equal : ⇒
the thesis becomes the hypothesis H1
subst0 (s k0 i0) v0 t1 t2
end of H10
(H12)
we proceed by induction on H8 to prove subst0 (s k i0) v0 t1 t2
case refl_equal : ⇒
the thesis becomes the hypothesis H10
subst0 (s k i0) v0 t1 t2
end of H12
by (refl_equal . .)
we proved eq T (THead k u1 t2) (THead k u1 t2)
by (ex_intro2 . . . . previous H12)
we proved ex2 T λt3:T.eq T (THead k u1 t2) (THead k u1 t3) λt3:T.subst0 (s k i0) v0 t1 t3
by (or3_intro1 . . . previous)
we proved
or3
ex2 T λu2:T.eq T (THead k u1 t2) (THead k u2 t1) λu2:T.subst0 i0 v0 u1 u2
ex2 T λt3:T.eq T (THead k u1 t2) (THead k u1 t3) λt3:T.subst0 (s k i0) v0 t1 t3
ex3_2 T T λu2:T.λt3:T.eq T (THead k u1 t2) (THead k u2 t3) λu2:T.λ:T.subst0 i0 v0 u1 u2 λ:T.λt3:T.subst0 (s k i0) v0 t1 t3
by (eq_ind_r . . . previous . H8)
we proved
or3
ex2 T λu2:T.eq T (THead k0 u1 t2) (THead k u2 t1) λu2:T.subst0 i0 v0 u1 u2
ex2 T λt3:T.eq T (THead k0 u1 t2) (THead k u1 t3) λt3:T.subst0 (s k i0) v0 t1 t3
ex3_2 T T λu2:T.λt3:T.eq T (THead k0 u1 t2) (THead k u2 t3) λu2:T.λ:T.subst0 i0 v0 u1 u2 λ:T.λt3:T.subst0 (s k i0) v0 t1 t3
by (eq_ind_r . . . previous . H7)
we proved
or3
ex2 T λu2:T.eq T (THead k0 u t2) (THead k u2 t1) λu2:T.subst0 i0 v0 u1 u2
ex2 T λt3:T.eq T (THead k0 u t2) (THead k u1 t3) λt3:T.subst0 (s k i0) v0 t1 t3
ex3_2 T T λu2:T.λt3:T.eq T (THead k0 u t2) (THead k u2 t3) λu2:T.λ:T.subst0 i0 v0 u1 u2 λ:T.λt3:T.subst0 (s k i0) v0 t1 t3
eq T u u1
→(eq K k0 k
→(or3
ex2 T λu2:T.eq T (THead k0 u t2) (THead k u2 t1) λu2:T.subst0 i0 v0 u1 u2
ex2 T λt3:T.eq T (THead k0 u t2) (THead k u1 t3) λt3:T.subst0 (s k i0) v0 t1 t3
ex3_2 T T λu2:T.λt3:T.eq T (THead k0 u t2) (THead k u2 t3) λu2:T.λ:T.subst0 i0 v0 u1 u2 λ:T.λt3:T.subst0 (s k i0) v0 t1 t3))
end of h1
(h2)
consider H5
we proved
eq
T
<λ:T.T> CASE THead k0 u t0 OF TSort ⇒u | TLRef ⇒u | THead t ⇒t
<λ:T.T> CASE THead k u1 t1 OF TSort ⇒u | TLRef ⇒u | THead t ⇒t
eq T u u1
end of h2
by (h1 h2)
eq K k0 k
→(or3
ex2 T λu2:T.eq T (THead k0 u t2) (THead k u2 t1) λu2:T.subst0 i0 v0 u1 u2
ex2 T λt3:T.eq T (THead k0 u t2) (THead k u1 t3) λt3:T.subst0 (s k i0) v0 t1 t3
ex3_2 T T λu2:T.λt3:T.eq T (THead k0 u t2) (THead k u2 t3) λu2:T.λ:T.subst0 i0 v0 u1 u2 λ:T.λt3:T.subst0 (s k i0) v0 t1 t3)
end of h1
(h2)
consider H4
we proved
eq
K
<λ:T.K> CASE THead k0 u t0 OF TSort ⇒k0 | TLRef ⇒k0 | THead k1 ⇒k1
<λ:T.K> CASE THead k u1 t1 OF TSort ⇒k0 | TLRef ⇒k0 | THead k1 ⇒k1
eq K k0 k
end of h2
by (h1 h2)
we proved
or3
ex2 T λu2:T.eq T (THead k0 u t2) (THead k u2 t1) λu2:T.subst0 i0 v0 u1 u2
ex2 T λt3:T.eq T (THead k0 u t2) (THead k u1 t3) λt3:T.subst0 (s k i0) v0 t1 t3
ex3_2 T T λu2:T.λt3:T.eq T (THead k0 u t2) (THead k u2 t3) λu2:T.λ:T.subst0 i0 v0 u1 u2 λ:T.λt3:T.subst0 (s k i0) v0 t1 t3
∀H3:eq T (THead k0 u t0) (THead k u1 t1)
.or3
ex2 T λu2:T.eq T (THead k0 u t2) (THead k u2 t1) λu2:T.subst0 i0 v0 u1 u2
ex2 T λt3:T.eq T (THead k0 u t2) (THead k u1 t3) λt3:T.subst0 (s k i0) v0 t1 t3
ex3_2 T T λu2:T.λt3:T.eq T (THead k0 u t2) (THead k u2 t3) λu2:T.λ:T.subst0 i0 v0 u1 u2 λ:T.λt3:T.subst0 (s k i0) v0 t1 t3
case subst0_both : v0:T u0:T u2:T i0:nat H1:subst0 i0 v0 u0 u2 k0:K t0:T t2:T H3:subst0 (s k0 i0) v0 t0 t2 ⇒
the thesis becomes
∀H5:eq T (THead k0 u0 t0) (THead k u1 t1)
.or3
ex2 T λu3:T.eq T (THead k0 u2 t2) (THead k u3 t1) λu3:T.subst0 i0 v0 u1 u3
ex2 T λt3:T.eq T (THead k0 u2 t2) (THead k u1 t3) λt3:T.subst0 (s k i0) v0 t1 t3
ex3_2 T T λu3:T.λt3:T.eq T (THead k0 u2 t2) (THead k u3 t3) λu3:T.λ:T.subst0 i0 v0 u1 u3 λ:T.λt3:T.subst0 (s k i0) v0 t1 t3
(H2) by induction hypothesis we know
eq T u0 (THead k u1 t1)
→(or3
ex2 T λu3:T.eq T u2 (THead k u3 t1) λu3:T.subst0 i0 v0 u1 u3
ex2 T λt2:T.eq T u2 (THead k u1 t2) λt2:T.subst0 (s k i0) v0 t1 t2
ex3_2 T T λu3:T.λt2:T.eq T u2 (THead k u3 t2) λu3:T.λ:T.subst0 i0 v0 u1 u3 λ:T.λt2:T.subst0 (s k i0) v0 t1 t2)
(H4) by induction hypothesis we know
eq T t0 (THead k u1 t1)
→(or3
ex2 T λu3:T.eq T t2 (THead k u3 t1) λu3:T.subst0 (s k0 i0) v0 u1 u3
ex2 T λt3:T.eq T t2 (THead k u1 t3) λt3:T.subst0 (s k (s k0 i0)) v0 t1 t3
ex3_2 T T λu3:T.λt3:T.eq T t2 (THead k u3 t3) λu3:T.λ:T.subst0 (s k0 i0) v0 u1 u3 λ:T.λt3:T.subst0 (s k (s k0 i0)) v0 t1 t3)
suppose H5: eq T (THead k0 u0 t0) (THead k u1 t1)
(H6)
by (f_equal . . . . . H5)
we proved
eq
K
<λ:T.K> CASE THead k0 u0 t0 OF TSort ⇒k0 | TLRef ⇒k0 | THead k1 ⇒k1
<λ:T.K> CASE THead k u1 t1 OF TSort ⇒k0 | TLRef ⇒k0 | THead k1 ⇒k1
eq
K
λe:T.<λ:T.K> CASE e OF TSort ⇒k0 | TLRef ⇒k0 | THead k1 ⇒k1 (THead k0 u0 t0)
λe:T.<λ:T.K> CASE e OF TSort ⇒k0 | TLRef ⇒k0 | THead k1 ⇒k1 (THead k u1 t1)
end of H6
(h1)
(H7)
by (f_equal . . . . . H5)
we proved
eq
T
<λ:T.T> CASE THead k0 u0 t0 OF TSort ⇒u0 | TLRef ⇒u0 | THead t ⇒t
<λ:T.T> CASE THead k u1 t1 OF TSort ⇒u0 | TLRef ⇒u0 | THead t ⇒t
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒u0 | TLRef ⇒u0 | THead t ⇒t (THead k0 u0 t0)
λe:T.<λ:T.T> CASE e OF TSort ⇒u0 | TLRef ⇒u0 | THead t ⇒t (THead k u1 t1)
end of H7
(h1)
(H8)
by (f_equal . . . . . H5)
we proved
eq
T
<λ:T.T> CASE THead k0 u0 t0 OF TSort ⇒t0 | TLRef ⇒t0 | THead t⇒t
<λ:T.T> CASE THead k u1 t1 OF TSort ⇒t0 | TLRef ⇒t0 | THead t⇒t
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t0 | TLRef ⇒t0 | THead t⇒t (THead k0 u0 t0)
λe:T.<λ:T.T> CASE e OF TSort ⇒t0 | TLRef ⇒t0 | THead t⇒t (THead k u1 t1)
end of H8
suppose H9: eq T u0 u1
suppose H10: eq K k0 k
(H11)
consider H8
we proved
eq
T
<λ:T.T> CASE THead k0 u0 t0 OF TSort ⇒t0 | TLRef ⇒t0 | THead t⇒t
<λ:T.T> CASE THead k u1 t1 OF TSort ⇒t0 | TLRef ⇒t0 | THead t⇒t
that is equivalent to eq T t0 t1
we proceed by induction on the previous result to prove
eq T t1 (THead k u1 t1)
→(or3
ex2 T λu3:T.eq T t2 (THead k u3 t1) λu3:T.subst0 (s k0 i0) v0 u1 u3
ex2 T λt3:T.eq T t2 (THead k u1 t3) λt3:T.subst0 (s k (s k0 i0)) v0 t1 t3
ex3_2 T T λu3:T.λt3:T.eq T t2 (THead k u3 t3) λu3:T.λ:T.subst0 (s k0 i0) v0 u1 u3 λ:T.λt3:T.subst0 (s k (s k0 i0)) v0 t1 t3)
case refl_equal : ⇒
the thesis becomes the hypothesis H4
eq T t1 (THead k u1 t1)
→(or3
ex2 T λu3:T.eq T t2 (THead k u3 t1) λu3:T.subst0 (s k0 i0) v0 u1 u3
ex2 T λt3:T.eq T t2 (THead k u1 t3) λt3:T.subst0 (s k (s k0 i0)) v0 t1 t3
ex3_2 T T λu3:T.λt3:T.eq T t2 (THead k u3 t3) λu3:T.λ:T.subst0 (s k0 i0) v0 u1 u3 λ:T.λt3:T.subst0 (s k (s k0 i0)) v0 t1 t3)
end of H11
(H12)
consider H8
we proved
eq
T
<λ:T.T> CASE THead k0 u0 t0 OF TSort ⇒t0 | TLRef ⇒t0 | THead t⇒t
<λ:T.T> CASE THead k u1 t1 OF TSort ⇒t0 | TLRef ⇒t0 | THead t⇒t
that is equivalent to eq T t0 t1
we proceed by induction on the previous result to prove subst0 (s k0 i0) v0 t1 t2
case refl_equal : ⇒
the thesis becomes the hypothesis H3
subst0 (s k0 i0) v0 t1 t2
end of H12
(H14)
we proceed by induction on H10 to prove subst0 (s k i0) v0 t1 t2
case refl_equal : ⇒
the thesis becomes the hypothesis H12
subst0 (s k i0) v0 t1 t2
end of H14
(H16)
we proceed by induction on H9 to prove subst0 i0 v0 u1 u2
case refl_equal : ⇒
the thesis becomes the hypothesis H1
subst0 i0 v0 u1 u2
end of H16
by (refl_equal . .)
we proved eq T (THead k u2 t2) (THead k u2 t2)
by (ex3_2_intro . . . . . . . previous H16 H14)
we proved ex3_2 T T λu3:T.λt3:T.eq T (THead k u2 t2) (THead k u3 t3) λu3:T.λ:T.subst0 i0 v0 u1 u3 λ:T.λt3:T.subst0 (s k i0) v0 t1 t3
by (or3_intro2 . . . previous)
we proved
or3
ex2 T λu3:T.eq T (THead k u2 t2) (THead k u3 t1) λu3:T.subst0 i0 v0 u1 u3
ex2 T λt3:T.eq T (THead k u2 t2) (THead k u1 t3) λt3:T.subst0 (s k i0) v0 t1 t3
ex3_2 T T λu3:T.λt3:T.eq T (THead k u2 t2) (THead k u3 t3) λu3:T.λ:T.subst0 i0 v0 u1 u3 λ:T.λt3:T.subst0 (s k i0) v0 t1 t3
by (eq_ind_r . . . previous . H10)
we proved
or3
ex2 T λu3:T.eq T (THead k0 u2 t2) (THead k u3 t1) λu3:T.subst0 i0 v0 u1 u3
ex2 T λt3:T.eq T (THead k0 u2 t2) (THead k u1 t3) λt3:T.subst0 (s k i0) v0 t1 t3
ex3_2 T T λu3:T.λt3:T.eq T (THead k0 u2 t2) (THead k u3 t3) λu3:T.λ:T.subst0 i0 v0 u1 u3 λ:T.λt3:T.subst0 (s k i0) v0 t1 t3
eq T u0 u1
→(eq K k0 k
→(or3
ex2 T λu3:T.eq T (THead k0 u2 t2) (THead k u3 t1) λu3:T.subst0 i0 v0 u1 u3
ex2 T λt3:T.eq T (THead k0 u2 t2) (THead k u1 t3) λt3:T.subst0 (s k i0) v0 t1 t3
ex3_2 T T λu3:T.λt3:T.eq T (THead k0 u2 t2) (THead k u3 t3) λu3:T.λ:T.subst0 i0 v0 u1 u3 λ:T.λt3:T.subst0 (s k i0) v0 t1 t3))
end of h1
(h2)
consider H7
we proved
eq
T
<λ:T.T> CASE THead k0 u0 t0 OF TSort ⇒u0 | TLRef ⇒u0 | THead t ⇒t
<λ:T.T> CASE THead k u1 t1 OF TSort ⇒u0 | TLRef ⇒u0 | THead t ⇒t
eq T u0 u1
end of h2
by (h1 h2)
eq K k0 k
→(or3
ex2 T λu3:T.eq T (THead k0 u2 t2) (THead k u3 t1) λu3:T.subst0 i0 v0 u1 u3
ex2 T λt3:T.eq T (THead k0 u2 t2) (THead k u1 t3) λt3:T.subst0 (s k i0) v0 t1 t3
ex3_2 T T λu3:T.λt3:T.eq T (THead k0 u2 t2) (THead k u3 t3) λu3:T.λ:T.subst0 i0 v0 u1 u3 λ:T.λt3:T.subst0 (s k i0) v0 t1 t3)
end of h1
(h2)
consider H6
we proved
eq
K
<λ:T.K> CASE THead k0 u0 t0 OF TSort ⇒k0 | TLRef ⇒k0 | THead k1 ⇒k1
<λ:T.K> CASE THead k u1 t1 OF TSort ⇒k0 | TLRef ⇒k0 | THead k1 ⇒k1
eq K k0 k
end of h2
by (h1 h2)
we proved
or3
ex2 T λu3:T.eq T (THead k0 u2 t2) (THead k u3 t1) λu3:T.subst0 i0 v0 u1 u3
ex2 T λt3:T.eq T (THead k0 u2 t2) (THead k u1 t3) λt3:T.subst0 (s k i0) v0 t1 t3
ex3_2 T T λu3:T.λt3:T.eq T (THead k0 u2 t2) (THead k u3 t3) λu3:T.λ:T.subst0 i0 v0 u1 u3 λ:T.λt3:T.subst0 (s k i0) v0 t1 t3
∀H5:eq T (THead k0 u0 t0) (THead k u1 t1)
.or3
ex2 T λu3:T.eq T (THead k0 u2 t2) (THead k u3 t1) λu3:T.subst0 i0 v0 u1 u3
ex2 T λt3:T.eq T (THead k0 u2 t2) (THead k u1 t3) λt3:T.subst0 (s k i0) v0 t1 t3
ex3_2 T T λu3:T.λt3:T.eq T (THead k0 u2 t2) (THead k u3 t3) λu3:T.λ:T.subst0 i0 v0 u1 u3 λ:T.λt3:T.subst0 (s k i0) v0 t1 t3
we proved
eq T y (THead k u1 t1)
→(or3
ex2 T λu2:T.eq T x (THead k u2 t1) λu2:T.subst0 i v u1 u2
ex2 T λt3:T.eq T x (THead k u1 t3) λt3:T.subst0 (s k i) v t1 t3
ex3_2 T T λu2:T.λt3:T.eq T x (THead k u2 t3) λu2:T.λ:T.subst0 i v u1 u2 λ:T.λt3:T.subst0 (s k i) v t1 t3)
we proved
∀y:T
.subst0 i v y x
→(eq T y (THead k u1 t1)
→(or3
ex2 T λu2:T.eq T x (THead k u2 t1) λu2:T.subst0 i v u1 u2
ex2 T λt3:T.eq T x (THead k u1 t3) λt3:T.subst0 (s k i) v t1 t3
ex3_2 T T λu2:T.λt3:T.eq T x (THead k u2 t3) λu2:T.λ:T.subst0 i v u1 u2 λ:T.λt3:T.subst0 (s k i) v t1 t3))
by (insert_eq . . . . previous H)
we proved
or3
ex2 T λu2:T.eq T x (THead k u2 t1) λu2:T.subst0 i v u1 u2
ex2 T λt2:T.eq T x (THead k u1 t2) λt2:T.subst0 (s k i) v t1 t2
ex3_2 T T λu2:T.λt2:T.eq T x (THead k u2 t2) λu2:T.λ:T.subst0 i v u1 u2 λ:T.λt2:T.subst0 (s k i) v t1 t2
we proved
∀k:K
.∀v:T
.∀u1:T
.∀t1:T
.∀x:T
.∀i:nat
.subst0 i v (THead k u1 t1) x
→(or3
ex2 T λu2:T.eq T x (THead k u2 t1) λu2:T.subst0 i v u1 u2
ex2 T λt2:T.eq T x (THead k u1 t2) λt2:T.subst0 (s k i) v t1 t2
ex3_2 T T λu2:T.λt2:T.eq T x (THead k u2 t2) λu2:T.λ:T.subst0 i v u1 u2 λ:T.λt2:T.subst0 (s k i) v t1 t2)