DEFINITION subst_lref_gt()
TYPE =
∀v:T
.∀d:nat
.∀i:nat
.(lt d i)→(eq T (subst d v (TLRef i)) (TLRef (pred i)))
BODY =
assume v: T
assume d: nat
assume i: nat
suppose H: lt d i
(h1)
(h1)
by (refl_equal . .)
we proved eq T (TLRef (pred i)) (TLRef (pred i))
eq
T
<λb1:bool.T> CASE true OF true⇒TLRef (pred i) | false⇒lift d O v
TLRef (pred i)
end of h1
(h2)
by (lt_blt . . H)
eq bool (blt d i) true
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
eq
T
<λb1:bool.T> CASE blt d i OF true⇒TLRef (pred i) | false⇒lift d O v
TLRef (pred i)
eq
T
<λb1:bool.T>
CASE false OF
true⇒TLRef i
| false⇒<λb1:bool.T> CASE blt d i OF true⇒TLRef (pred i) | false⇒lift d O v
TLRef (pred i)
end of h1
(h2)
by (lt_le_weak . . H)
we proved le d i
by (le_bge . . previous)
eq bool (blt i d) false
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
eq
T
<λb1:bool.T>
CASE blt i d OF
true⇒TLRef i
| false⇒<λb1:bool.T> CASE blt d i OF true⇒TLRef (pred i) | false⇒lift d O v
TLRef (pred i)
that is equivalent to eq T (subst d v (TLRef i)) (TLRef (pred i))
we proved
∀v:T
.∀d:nat
.∀i:nat
.(lt d i)→(eq T (subst d v (TLRef i)) (TLRef (pred i)))