---

Step * of Lemma length-remove-first-le

∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)}  ⟶ 𝔹].  (||remove-first(P;L)|| ≤ ||L||)
BY
{ InstLemma `length-remove-first` []
THEN RepeatFor 3 (ParallelLast')
THEN D -1
THEN ExRepD
THEN HypSubst' -1 0
THEN Auto }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[P:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbB{}].    (||remove-first(P;L)||  \mleq{}  ||L||)


By

---

Latex:
InstLemma  `length-remove-first`  []
THEN  RepeatFor  3  (ParallelLast')
THEN  D  -1
THEN  ExRepD
THEN  HypSubst'  -1  0
THEN  Auto

---

Home Index