---

Step * of Lemma context-lookup-stable1

∀[Gamma,more:mFOL() List]. ∀[x:ℕ||Gamma||].  (context-lookup(more @ Gamma;x) ~ context-lookup(Gamma;x))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `context-lookup` 0
   THEN (RWO "length-append" 0 THENA Auto)
   THEN (RWO "select-append" 0 THENA Auto)) }

1
1. Gamma : mFOL() List
2. more : mFOL() List
3. x : ℕ||Gamma||
⊢ if (||more|| + ||Gamma||) - x + 1 <z ||more||
then more[(||more|| + ||Gamma||) - x + 1]
else Gamma[(||more|| + ||Gamma||) - x + 1 - ||more||]
fi  ~ Gamma[||Gamma|| - x + 1]

---

Latex:

---

Latex:
\mforall{}[Gamma,more:mFOL()  List].  \mforall{}[x:\mBbbN{}||Gamma||].
    (context-lookup(more  @  Gamma;x)  \msim{}  context-lookup(Gamma;x))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `context-lookup`  0
  THEN  (RWO  "length-append"  0  THENA  Auto)
  THEN  (RWO  "select-append"  0  THENA  Auto))

---

Home Index