---

Step * of Lemma remove_leading_property

∀[T:Type]. ∀L:T List. ∀P:T ⟶ 𝔹.  ∃xs:{x:T| ↑P[x]}  List. (L = (xs @ remove_leading(x.P[x];L)) ∈ (T List))
BY
{ xxx(InductionOnList THEN Reduce 0 THEN (D 0 THENA Auto))xxx }

1
1. [T] : Type
2. P : T ⟶ 𝔹
⊢ ∃xs:{x:T| ↑P[x]}  List. ([] = (xs @ remove_leading(x.P[x];[])) ∈ (T List))

2
1. [T] : Type
2. u : T
3. v : T List
4. ∀P:T ⟶ 𝔹. ∃xs:{x:T| ↑P[x]}  List. (v = (xs @ remove_leading(x.P[x];v)) ∈ (T List))
5. P : T ⟶ 𝔹
⊢ ∃xs:{x:T| ↑P[x]}  List. ([u / v] = (xs @ remove_leading(x.P[x];[u / v])) ∈ (T List))

---

Latex:

---

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


By

---

Latex:
xxx(InductionOnList  THEN  Reduce  0  THEN  (D  0  THENA  Auto))xxx

---

Home Index