DEFINITION subst_lift_SO()
TYPE =
∀v:T.∀t:T.∀d:nat.(eq T (subst d v (lift (S O) d t)) t)
BODY =
assume v: T
assume t: T
we proceed by induction on t to prove ∀d:nat.(eq T (subst d v (lift (S O) d t)) t)
case TSort : n:nat ⇒
the thesis becomes ∀d:nat.(eq T (subst d v (lift (S O) d (TSort n))) (TSort n))
assume d: nat
(h1)
(h1)
by (refl_equal . .)
eq T (TSort n) (TSort n)
end of h1
(h2)
by (subst_sort . . .)
eq T (subst d v (TSort n)) (TSort n)
end of h2
by (eq_ind_r . . . h1 . h2)
eq T (subst d v (TSort n)) (TSort n)
end of h1
(h2)
by (lift_sort . . .)
eq T (lift (S O) d (TSort n)) (TSort n)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved eq T (subst d v (lift (S O) d (TSort n))) (TSort n)
∀d:nat.(eq T (subst d v (lift (S O) d (TSort n))) (TSort n))
case TLRef : n:nat ⇒
the thesis becomes ∀d:nat.(eq T (subst d v (lift (S O) d (TLRef n))) (TLRef n))
assume d: nat
(h1)
suppose H: lt n d
(h1)
(h1)
by (refl_equal . .)
eq T (TLRef n) (TLRef n)
end of h1
(h2)
by (subst_lref_lt . . . H)
eq T (subst d v (TLRef n)) (TLRef n)
end of h2
by (eq_ind_r . . . h1 . h2)
eq T (subst d v (TLRef n)) (TLRef n)
end of h1
(h2)
by (lift_lref_lt . . . H)
eq T (lift (S O) d (TLRef n)) (TLRef n)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved eq T (subst d v (lift (S O) d (TLRef n))) (TLRef n)
lt n d
→eq T (subst d v (lift (S O) d (TLRef n))) (TLRef n)
end of h1
(h2)
suppose H: le d n
(h1)
by (plus_n_Sm . .)
we proved eq nat (S (plus n O)) (plus n (S O))
we proceed by induction on the previous result to prove eq T (subst d v (TLRef (plus n (S O)))) (TLRef n)
case refl_equal : ⇒
the thesis becomes eq T (subst d v (TLRef (S (plus n O)))) (TLRef n)
(h1)
by (pred_Sn .)
we proved eq nat (plus n O) (pred (S (plus n O)))
we proceed by induction on the previous result to prove eq T (TLRef (pred (S (plus n O)))) (TLRef n)
case refl_equal : ⇒
the thesis becomes eq T (TLRef (plus n O)) (TLRef n)
by (plus_n_O .)
we proved eq nat n (plus n O)
by (sym_eq . . . previous)
we proved eq nat (plus n O) n
by (f_equal . . . . . previous)
eq T (TLRef (plus n O)) (TLRef n)
eq T (TLRef (pred (S (plus n O)))) (TLRef n)
end of h1
(h2)
by (le_plus_trans . . . H)
we proved le d (plus n O)
by (le_n_S . . previous)
we proved le (S d) (S (plus n O))
that is equivalent to lt d (S (plus n O))
by (subst_lref_gt . . . previous)
eq
T
subst d v (TLRef (S (plus n O)))
TLRef (pred (S (plus n O)))
end of h2
by (eq_ind_r . . . h1 . h2)
eq T (subst d v (TLRef (S (plus n O)))) (TLRef n)
eq T (subst d v (TLRef (plus n (S O)))) (TLRef n)
end of h1
(h2)
by (lift_lref_ge . . . H)
eq T (lift (S O) d (TLRef n)) (TLRef (plus n (S O)))
end of h2
by (eq_ind_r . . . h1 . h2)
we proved eq T (subst d v (lift (S O) d (TLRef n))) (TLRef n)
le d n
→eq T (subst d v (lift (S O) d (TLRef n))) (TLRef n)
end of h2
by (lt_le_e . . . h1 h2)
we proved eq T (subst d v (lift (S O) d (TLRef n))) (TLRef n)
∀d:nat.(eq T (subst d v (lift (S O) d (TLRef n))) (TLRef n))
case THead : k:K t0:T t1:T ⇒
the thesis becomes ∀d:nat.(eq T (subst d v (lift (S O) d (THead k t0 t1))) (THead k t0 t1))
(H) by induction hypothesis we know ∀d:nat.(eq T (subst d v (lift (S O) d t0)) t0)
(H0) by induction hypothesis we know ∀d:nat.(eq T (subst d v (lift (S O) d t1)) t1)
assume d: nat
(h1)
(h1)
(h1)
by (refl_equal . .)
eq K k k
end of h1
(h2)
by (H .)
eq T (subst d v (lift (S O) d t0)) t0
end of h2
(h3)
by (H0 .)
eq T (subst (s k d) v (lift (S O) (s k d) t1)) t1
end of h3
by (f_equal3 . . . . . . . . . . . h1 h2 h3)
eq
T
THead
k
subst d v (lift (S O) d t0)
subst (s k d) v (lift (S O) (s k d) t1)
THead k t0 t1
end of h1
(h2)
by (subst_head . . . . .)
eq
T
subst d v (THead k (lift (S O) d t0) (lift (S O) (s k d) t1))
THead
k
subst d v (lift (S O) d t0)
subst (s k d) v (lift (S O) (s k d) t1)
end of h2
by (eq_ind_r . . . h1 . h2)
eq
T
subst d v (THead k (lift (S O) d t0) (lift (S O) (s k d) t1))
THead k t0 t1
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift (S O) d (THead k t0 t1)
THead k (lift (S O) d t0) (lift (S O) (s k d) t1)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved eq T (subst d v (lift (S O) d (THead k t0 t1))) (THead k t0 t1)
∀d:nat.(eq T (subst d v (lift (S O) d (THead k t0 t1))) (THead k t0 t1))
we proved ∀d:nat.(eq T (subst d v (lift (S O) d t)) t)
we proved ∀v:T.∀t:T.∀d:nat.(eq T (subst d v (lift (S O) d t)) t)