---

Step * of Lemma pos-length

∀[A:Type]. ∀[l:A List].  uiff(¬(l = [] ∈ (A List));0 < ||l||)
BY
{ (Auto THEN Try ((InstLemma `pos_length` [⌜A⌝;⌜l⌝]⋅ THEN Complete (Auto)))) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[l:A  List].    uiff(\mneg{}(l  =  []);0  <  ||l||)


By

---

Latex:
(Auto  THEN  Try  ((InstLemma  `pos\_length`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{}]\mcdot{}  THEN  Complete  (Auto))))

---

Home Index