---

Step * 1 of Lemma whole_segment


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

---

Latex:

---

Latex:

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


By

---

Latex:
(RWO  "lapp\_fact\_b<"  0  THEN  Auto\{1,3\}-1)

---

Home Index