---

Step * 1 of Lemma whole_segment_example


1. T : Type
2. as : T List
⊢ (Π 0 ≤ k < ||as||. [as[k]]) = as ∈ (T List)
BY
{ (RWO "lapp_fact_b<" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  T  List
\mvdash{}  (\mPi{}  0  \mleq{}  k  <  ||as||.  [as[k]])  =  as


By

---

Latex:
(RWO  "lapp\_fact\_b<"  0  THEN  Auto)

---

Home Index