---

Step * of Lemma trivial-mklist

∀[T:Type]. ∀[L:T List]. ∀[f:ℕ||L|| ⟶ T].  mklist(||L||;f) = L ∈ (T List) supposing ∀i:ℕ||L||. ((f i) = L[i] ∈ T)
BY
{ (Auto THEN BLemma `list_extensionality` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[f:\mBbbN{}||L||  {}\mrightarrow{}  T].    mklist(||L||;f)  =  L  supposing  \mforall{}i:\mBbbN{}||L||.  ((f  i)  =  L[i])


By

---

Latex:
(Auto  THEN  BLemma  `list\_extensionality`  THEN  Auto)

---

Home Index