---

Step * of Lemma A-shift-upto_wf

∀[Val:Type]. ∀[n:ℕ].  (1 < n ⇒ (∀[AType:array{i:l}(Val;n)]. ∀[j:ℕn].  (A-shift-upto(AType;j) ∈ A-map Unit)))
BY
{ (ProveWfLemma
   THEN (Assert A-coerce(array-model(AType)) (A-fetch'(array-model(AType)) i) ∈ A-map Val BY
               Auto)
   THEN (Assert λin@i.(A-assign(array-model(AType)) (i - 1) in@i) ∈ Val ⟶ (A-map Unit) BY
               Auto)⋅
   THEN (InstLemma `A-bind_wf` [⌜Val⌝;⌜n⌝;⌜AType⌝;⌜Val⌝;⌜Unit⌝]⋅ THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[Val:Type].  \mforall{}[n:\mBbbN{}].
    (1  <  n  {}\mRightarrow{}  (\mforall{}[AType:array\{i:l\}(Val;n)].  \mforall{}[j:\mBbbN{}n].    (A-shift-upto(AType;j)  \mmember{}  A-map  Unit)))


By

---

Latex:
(ProveWfLemma
  THEN  (Assert  A-coerce(array-model(AType))  (A-fetch'(array-model(AType))  i)  \mmember{}  A-map  Val  BY
                          Auto)
  THEN  (Assert  \mlambda{}in@i.(A-assign(array-model(AType))  (i  -  1)  in@i)  \mmember{}  Val  {}\mrightarrow{}  (A-map  Unit)  BY
                          Auto)\mcdot{}
  THEN  (InstLemma  `A-bind\_wf`  [\mkleeneopen{}Val\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}AType\mkleeneclose{};\mkleeneopen{}Val\mkleeneclose{};\mkleeneopen{}Unit\mkleeneclose{}]\mcdot{}  THEN  Auto)\mcdot{})

---

Home Index