---

Step * of Lemma map-index_wf

∀[A,B:Type]. ∀[L:A List]. ∀[f:ℕ||L|| ⟶ {a:A| (a ∈ L)}  ⟶ B].  (map-index(f;L) ∈ B List)
BY
{ (Auto
   THEN Unfold `map-index` 0
   THEN (InstLemma `map-index_aux_wf` [⌜{a:A| (a ∈ L)} ⌝]⋅ THENA Auto)
   THEN BHyp -1 
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[L:A  List].  \mforall{}[f:\mBbbN{}||L||  {}\mrightarrow{}  \{a:A|  (a  \mmember{}  L)\}    {}\mrightarrow{}  B].    (map-index(f;L)  \mmember{}  B  List)


By

---

Latex:
(Auto
  THEN  Unfold  `map-index`  0
  THEN  (InstLemma  `map-index\_aux\_wf`  [\mkleeneopen{}\{a:A|  (a  \mmember{}  L)\}  \mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  BHyp  -1 
  THEN  Auto)

---

Home Index