---

Step * of Lemma select_reject_permr

∀T:Type. ∀as:T List. ∀i:ℕ||as||.  ([as[i] / as\[i]] ≡(T) as)
BY
{ (UnivCD THENA Auto) }

1
1. T : Type
2. as : T List
3. i : ℕ||as||
⊢ [as[i] / as\[i]] ≡(T) as

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}as:T  List.  \mforall{}i:\mBbbN{}||as||.    ([as[i]  /  as\mbackslash{}[i]]  \mequiv{}(T)  as)


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index