---

Step * of Lemma remove_leading_eq_nil

∀[T:Type]. ∀[L:T List]. ∀[P:T ⟶ 𝔹].  uiff(remove_leading(x.P[x];L) = [] ∈ (T List);(∀x∈L.↑P[x]))
BY
{ ((UnivCD THENA Auto)
   THEN (RWO "null_remove_leading<" 0 THENM RW assert_pushdownC 0)
   THEN Auto
   THEN Try ((D -2 THEN All Reduce THEN Auto'))) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RWO  "null\_remove\_leading<"  0  THENM  RW  assert\_pushdownC  0)
  THEN  Auto
  THEN  Try  ((D  -2  THEN  All  Reduce  THEN  Auto')))

---

Home Index