DEFINITION subst0_gen_lref()
TYPE =
∀v:T
.∀x:T
.∀i:nat
.∀n:nat
.subst0 i v (TLRef n) x
→land (eq nat n i) (eq T x (lift (S n) O v))
BODY =
assume v: T
assume x: T
assume i: nat
assume n: nat
suppose H: subst0 i v (TLRef n) x
assume y: T
suppose H0: subst0 i v y x
we proceed by induction on H0 to prove
eq T y (TLRef n)
→land (eq nat n i) (eq T x (lift (S n) O v))
case subst0_lref : v0:T i0:nat ⇒
the thesis becomes
∀H1:eq T (TLRef i0) (TLRef n)
.land (eq nat n i0) (eq T (lift (S i0) O v0) (lift (S n) O v0))
suppose H1: eq T (TLRef i0) (TLRef n)
(H2)
by (f_equal . . . . . H1)
we proved
eq
nat
<λ:T.nat> CASE TLRef i0 OF TSort ⇒i0 | TLRef n0⇒n0 | THead ⇒i0
<λ:T.nat> CASE TLRef n OF TSort ⇒i0 | TLRef n0⇒n0 | THead ⇒i0
eq
nat
λe:T.<λ:T.nat> CASE e OF TSort ⇒i0 | TLRef n0⇒n0 | THead ⇒i0 (TLRef i0)
λe:T.<λ:T.nat> CASE e OF TSort ⇒i0 | TLRef n0⇒n0 | THead ⇒i0 (TLRef n)
end of H2
(h1)
(h1)
by (refl_equal . .)
eq nat n n
end of h1
(h2)
by (refl_equal . .)
eq T (lift (S n) O v0) (lift (S n) O v0)
end of h2
by (conj . . h1 h2)
land (eq nat n n) (eq T (lift (S n) O v0) (lift (S n) O v0))
end of h1
(h2)
consider H2
we proved
eq
nat
<λ:T.nat> CASE TLRef i0 OF TSort ⇒i0 | TLRef n0⇒n0 | THead ⇒i0
<λ:T.nat> CASE TLRef n OF TSort ⇒i0 | TLRef n0⇒n0 | THead ⇒i0
eq nat i0 n
end of h2
by (eq_ind_r . . . h1 . h2)
we proved land (eq nat n i0) (eq T (lift (S i0) O v0) (lift (S n) O v0))
∀H1:eq T (TLRef i0) (TLRef n)
.land (eq nat n i0) (eq T (lift (S i0) O v0) (lift (S n) O v0))
case subst0_fst : v0:T u2:T u1:T i0:nat :subst0 i0 v0 u1 u2 t:T k:K ⇒
the thesis becomes
∀H3:eq T (THead k u1 t) (TLRef n)
.land (eq nat n i0) (eq T (THead k u2 t) (lift (S n) O v0))
() by induction hypothesis we know
(eq T u1 (TLRef n))→(land (eq nat n i0) (eq T u2 (lift (S n) O v0)))
suppose H3: eq T (THead k u1 t) (TLRef n)
(H4)
we proceed by induction on H3 to prove
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead k u1 t OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead k u1 t OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
end of H4
consider H4
we proved
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove land (eq nat n i0) (eq T (THead k u2 t) (lift (S n) O v0))
we proved land (eq nat n i0) (eq T (THead k u2 t) (lift (S n) O v0))
∀H3:eq T (THead k u1 t) (TLRef n)
.land (eq nat n i0) (eq T (THead k u2 t) (lift (S n) O v0))
case subst0_snd : k:K v0:T t2:T t1:T i0:nat :subst0 (s k i0) v0 t1 t2 u:T ⇒
the thesis becomes
∀H3:eq T (THead k u t1) (TLRef n)
.land (eq nat n i0) (eq T (THead k u t2) (lift (S n) O v0))
() by induction hypothesis we know
eq T t1 (TLRef n)
→land (eq nat n (s k i0)) (eq T t2 (lift (S n) O v0))
suppose H3: eq T (THead k u t1) (TLRef n)
(H4)
we proceed by induction on H3 to prove
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead k u t1 OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead k u t1 OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
end of H4
consider H4
we proved
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove land (eq nat n i0) (eq T (THead k u t2) (lift (S n) O v0))
we proved land (eq nat n i0) (eq T (THead k u t2) (lift (S n) O v0))
∀H3:eq T (THead k u t1) (TLRef n)
.land (eq nat n i0) (eq T (THead k u t2) (lift (S n) O v0))
case subst0_both : v0:T u1:T u2:T i0:nat :subst0 i0 v0 u1 u2 k:K t1:T t2:T :subst0 (s k i0) v0 t1 t2 ⇒
the thesis becomes
∀H5:eq T (THead k u1 t1) (TLRef n)
.land (eq nat n i0) (eq T (THead k u2 t2) (lift (S n) O v0))
() by induction hypothesis we know
(eq T u1 (TLRef n))→(land (eq nat n i0) (eq T u2 (lift (S n) O v0)))
() by induction hypothesis we know
eq T t1 (TLRef n)
→land (eq nat n (s k i0)) (eq T t2 (lift (S n) O v0))
suppose H5: eq T (THead k u1 t1) (TLRef n)
(H6)
we proceed by induction on H5 to prove
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead k u1 t1 OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead k u1 t1 OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
end of H6
consider H6
we proved
<λ:T.Prop>
CASE TLRef n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove land (eq nat n i0) (eq T (THead k u2 t2) (lift (S n) O v0))
we proved land (eq nat n i0) (eq T (THead k u2 t2) (lift (S n) O v0))
∀H5:eq T (THead k u1 t1) (TLRef n)
.land (eq nat n i0) (eq T (THead k u2 t2) (lift (S n) O v0))
we proved
eq T y (TLRef n)
→land (eq nat n i) (eq T x (lift (S n) O v))
we proved
∀y:T
.subst0 i v y x
→(eq T y (TLRef n)
→land (eq nat n i) (eq T x (lift (S n) O v)))
by (insert_eq . . . . previous H)
we proved land (eq nat n i) (eq T x (lift (S n) O v))
we proved
∀v:T
.∀x:T
.∀i:nat
.∀n:nat
.subst0 i v (TLRef n) x
→land (eq nat n i) (eq T x (lift (S n) O v))