---

Step * of Lemma cons_iseg_not_null

∀[T:Type]. ∀u:T. ∀L,v:T List.  (L ≤ [u / v] ⇒ (¬↑null(L)) ⇒ (∃K:T List. ((L = [u / K] ∈ (T List)) ∧ K ≤ v)))
BY
{ (Auto
   THEN D (-4)
   THEN AllReduce
   THEN Try (Trivial)
   THEN (RWO "cons_iseg" (-2) THENA Auto)
   THEN RepD
   THEN InstConcl [⌜v1⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}u:T.  \mforall{}L,v:T  List.    (L  \mleq{}  [u  /  v]  {}\mRightarrow{}  (\mneg{}\muparrow{}null(L))  {}\mRightarrow{}  (\mexists{}K:T  List.  ((L  =  [u  /  K])  \mwedge{}  K  \mleq{}  v)))


By

---

Latex:
(Auto
  THEN  D  (-4)
  THEN  AllReduce
  THEN  Try  (Trivial)
  THEN  (RWO  "cons\_iseg"  (-2)  THENA  Auto)
  THEN  RepD
  THEN  InstConcl  [\mkleeneopen{}v1\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index