---

Step * of Lemma list-decomp-nat-iseg

∀[T:Type]. ∀L:T List. ∀i:ℕ||L|| + 1.  ∃K:T List. (K ≤ L ∧ (||K|| = i ∈ ℤ))
BY
{ (Auto
   THEN (InstLemma `list-decomp-nat` [⌜T⌝;⌜L⌝;⌜i⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN InstConcl [⌜K⌝]⋅
   THEN Auto
   THEN UnfoldTopAb 0
   THEN InstConcl [⌜J⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}i:\mBbbN{}||L||  +  1.    \mexists{}K:T  List.  (K  \mleq{}  L  \mwedge{}  (||K||  =  i))


By

---

Latex:
(Auto
  THEN  (InstLemma  `list-decomp-nat`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  InstConcl  [\mkleeneopen{}K\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  UnfoldTopAb  0
  THEN  InstConcl  [\mkleeneopen{}J\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index