DEFINITION subst0_refl()
TYPE =
∀u:T.∀t:T.∀d:nat.(subst0 d u t t)→∀P:Prop.P
BODY =
assume u: T
assume t: T
we proceed by induction on t to prove ∀d:nat.(subst0 d u t t)→∀P:Prop.P
case TSort : n:nat ⇒
the thesis becomes ∀d:nat.∀H:(subst0 d u (TSort n) (TSort n)).∀P:Prop.P
assume d: nat
suppose H: subst0 d u (TSort n) (TSort n)
assume P: Prop
by (subst0_gen_sort . . . . H .)
we proved P
∀d:nat.∀H:(subst0 d u (TSort n) (TSort n)).∀P:Prop.P
case TLRef : n:nat ⇒
the thesis becomes ∀d:nat.∀H:(subst0 d u (TLRef n) (TLRef n)).∀P:Prop.P
assume d: nat
suppose H: subst0 d u (TLRef n) (TLRef n)
assume P: Prop
by (subst0_gen_lref . . . . H)
we proved land (eq nat n d) (eq T (TLRef n) (lift (S n) O u))
we proceed by induction on the previous result to prove P
case conj : :eq nat n d H1:eq T (TLRef n) (lift (S n) O u) ⇒
the thesis becomes P
(h1) by (le_O_n .) we proved le O n
(h2)
by (le_n .)
we proved le (plus O (S n)) (plus O (S n))
lt n (plus O (S n))
end of h2
by (lift_gen_lref_false . . . h1 h2 . H1 .)
P
we proved P
∀d:nat.∀H:(subst0 d u (TLRef n) (TLRef n)).∀P:Prop.P
case THead : k:K t0:T t1:T ⇒
the thesis becomes ∀d:nat.∀H1:(subst0 d u (THead k t0 t1) (THead k t0 t1)).∀P:Prop.P
(H) by induction hypothesis we know ∀d:nat.(subst0 d u t0 t0)→∀P:Prop.P
(H0) by induction hypothesis we know ∀d:nat.(subst0 d u t1 t1)→∀P:Prop.P
assume d: nat
suppose H1: subst0 d u (THead k t0 t1) (THead k t0 t1)
assume P: Prop
by (subst0_gen_head . . . . . . H1)
we proved
or3
ex2 T λu2:T.eq T (THead k t0 t1) (THead k u2 t1) λu2:T.subst0 d u t0 u2
ex2 T λt2:T.eq T (THead k t0 t1) (THead k t0 t2) λt2:T.subst0 (s k d) u t1 t2
ex3_2 T T λu2:T.λt2:T.eq T (THead k t0 t1) (THead k u2 t2) λu2:T.λ:T.subst0 d u t0 u2 λ:T.λt2:T.subst0 (s k d) u t1 t2
we proceed by induction on the previous result to prove P
case or3_intro0 : H2:ex2 T λu2:T.eq T (THead k t0 t1) (THead k u2 t1) λu2:T.subst0 d u t0 u2 ⇒
the thesis becomes P
we proceed by induction on H2 to prove P
case ex_intro2 : x:T H3:eq T (THead k t0 t1) (THead k x t1) H4:subst0 d u t0 x ⇒
the thesis becomes P
(H5)
by (f_equal . . . . . H3)
we proved
eq
T
<λ:T.T> CASE THead k t0 t1 OF TSort ⇒t0 | TLRef ⇒t0 | THead t2 ⇒t2
<λ:T.T> CASE THead k x t1 OF TSort ⇒t0 | TLRef ⇒t0 | THead t2 ⇒t2
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t0 | TLRef ⇒t0 | THead t2 ⇒t2 (THead k t0 t1)
λe:T.<λ:T.T> CASE e OF TSort ⇒t0 | TLRef ⇒t0 | THead t2 ⇒t2 (THead k x t1)
end of H5
(H6)
consider H5
we proved
eq
T
<λ:T.T> CASE THead k t0 t1 OF TSort ⇒t0 | TLRef ⇒t0 | THead t2 ⇒t2
<λ:T.T> CASE THead k x t1 OF TSort ⇒t0 | TLRef ⇒t0 | THead t2 ⇒t2
that is equivalent to eq T t0 x
by (eq_ind_r . . . H4 . previous)
subst0 d u t0 t0
end of H6
by (H . H6 .)
P
P
case or3_intro1 : H2:ex2 T λt2:T.eq T (THead k t0 t1) (THead k t0 t2) λt2:T.subst0 (s k d) u t1 t2 ⇒
the thesis becomes P
we proceed by induction on H2 to prove P
case ex_intro2 : x:T H3:eq T (THead k t0 t1) (THead k t0 x) H4:subst0 (s k d) u t1 x ⇒
the thesis becomes P
(H5)
by (f_equal . . . . . H3)
we proved
eq
T
<λ:T.T> CASE THead k t0 t1 OF TSort ⇒t1 | TLRef ⇒t1 | THead t2⇒t2
<λ:T.T> CASE THead k t0 x OF TSort ⇒t1 | TLRef ⇒t1 | THead t2⇒t2
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t1 | TLRef ⇒t1 | THead t2⇒t2 (THead k t0 t1)
λe:T.<λ:T.T> CASE e OF TSort ⇒t1 | TLRef ⇒t1 | THead t2⇒t2 (THead k t0 x)
end of H5
(H6)
consider H5
we proved
eq
T
<λ:T.T> CASE THead k t0 t1 OF TSort ⇒t1 | TLRef ⇒t1 | THead t2⇒t2
<λ:T.T> CASE THead k t0 x OF TSort ⇒t1 | TLRef ⇒t1 | THead t2⇒t2
that is equivalent to eq T t1 x
by (eq_ind_r . . . H4 . previous)
subst0 (s k d) u t1 t1
end of H6
by (H0 . H6 .)
P
P
case or3_intro2 : H2:ex3_2 T T λu2:T.λt2:T.eq T (THead k t0 t1) (THead k u2 t2) λu2:T.λ:T.subst0 d u t0 u2 λ:T.λt2:T.subst0 (s k d) u t1 t2 ⇒
the thesis becomes P
we proceed by induction on H2 to prove P
case ex3_2_intro : x0:T x1:T H3:eq T (THead k t0 t1) (THead k x0 x1) H4:subst0 d u t0 x0 H5:subst0 (s k d) u t1 x1 ⇒
the thesis becomes P
(H6)
by (f_equal . . . . . H3)
we proved
eq
T
<λ:T.T> CASE THead k t0 t1 OF TSort ⇒t0 | TLRef ⇒t0 | THead t2 ⇒t2
<λ:T.T> CASE THead k x0 x1 OF TSort ⇒t0 | TLRef ⇒t0 | THead t2 ⇒t2
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t0 | TLRef ⇒t0 | THead t2 ⇒t2 (THead k t0 t1)
λe:T.<λ:T.T> CASE e OF TSort ⇒t0 | TLRef ⇒t0 | THead t2 ⇒t2 (THead k x0 x1)
end of H6
(h1)
(H7)
by (f_equal . . . . . H3)
we proved
eq
T
<λ:T.T> CASE THead k t0 t1 OF TSort ⇒t1 | TLRef ⇒t1 | THead t2⇒t2
<λ:T.T> CASE THead k x0 x1 OF TSort ⇒t1 | TLRef ⇒t1 | THead t2⇒t2
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t1 | TLRef ⇒t1 | THead t2⇒t2 (THead k t0 t1)
λe:T.<λ:T.T> CASE e OF TSort ⇒t1 | TLRef ⇒t1 | THead t2⇒t2 (THead k x0 x1)
end of H7
suppose H8: eq T t0 x0
(H10)
by (eq_ind_r . . . H4 . H8)
subst0 d u t0 t0
end of H10
by (H . H10 .)
we proved P
(eq T t0 x0)→P
end of h1
(h2)
consider H6
we proved
eq
T
<λ:T.T> CASE THead k t0 t1 OF TSort ⇒t0 | TLRef ⇒t0 | THead t2 ⇒t2
<λ:T.T> CASE THead k x0 x1 OF TSort ⇒t0 | TLRef ⇒t0 | THead t2 ⇒t2
eq T t0 x0
end of h2
by (h1 h2)
P
P
we proved P
∀d:nat.∀H1:(subst0 d u (THead k t0 t1) (THead k t0 t1)).∀P:Prop.P
we proved ∀d:nat.(subst0 d u t t)→∀P:Prop.P
we proved ∀u:T.∀t:T.∀d:nat.(subst0 d u t t)→∀P:Prop.P