---

Step * 1 of Lemma remove_leading_property


1. [T] : Type
2. P : T ⟶ 𝔹
⊢ ∃xs:{x:T| ↑P[x]}  List. ([] = (xs @ remove_leading(x.P[x];[])) ∈ (T List))
BY
{ xxx(RepUR ``remove_leading`` 0 THEN With ⌜[]⌝ (D 0)⋅ THEN Auto)xxx }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
\mvdash{}  \mexists{}xs:\{x:T|  \muparrow{}P[x]\}    List.  ([]  =  (xs  @  remove\_leading(x.P[x];[])))


By

---

Latex:
xxx(RepUR  ``remove\_leading``  0  THEN  With  \mkleeneopen{}[]\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)xxx

---

Home Index