---

Step * of Lemma list_decomp_reverse

∀[T:Type]. ∀L:T List. ∃x:T. ∃L':T List. (L = (L' @ [x]) ∈ (T List)) supposing 0 < ||L||
BY
{ (InductionOnList THEN Reduce 0 THEN Auto THEN Thin (-1)) }

1
1. [T] : Type
2. u : T
3. v : T List
4. ∃x:T. ∃L':T List. (v = (L' @ [x]) ∈ (T List)) supposing 0 < ||v||
⊢ ∃x:T. ∃L':T List. ([u / v] = (L' @ [x]) ∈ (T List))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mexists{}x:T.  \mexists{}L':T  List.  (L  =  (L'  @  [x]))  supposing  0  <  ||L||


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  Auto  THEN  Thin  (-1))

---

Home Index