---

Step * of Lemma list_decomp_rev_wf

∀[T:Type]. ∀[l:T List].  list_decomp_rev{i:l}(l) ∈ {p:T × (T List)| l = ((snd(p)) @ [fst(p)]) ∈ (T List)}  supposing 0 <\000C ||l||
BY
{ (Auto
   THEN RepUR ``list_decomp_rev`` 0
   THEN GenConclAtAddr [2;1;1]
   THEN (With ⌜T⌝ (D (-2))⋅ THENA Auto)
   THEN (GenConclAtAddrType ⌜∃x:T. ∃L':T List. (l = (L' @ [x]) ∈ (T List))⌝ [2;1]⋅ THENA Auto)
   THEN ExRepD
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[l:T  List].    list\_decomp\_rev\{i:l\}(l)  \mmember{}  \{p:T  \mtimes{}  (T  List)|  l  =  ((snd(p))  @  [fst(p)])\}    supp\000Cosing  0  <  ||l||


By

---

Latex:
(Auto
  THEN  RepUR  ``list\_decomp\_rev``  0
  THEN  GenConclAtAddr  [2;1;1]
  THEN  (With  \mkleeneopen{}T\mkleeneclose{}  (D  (-2))\mcdot{}  THENA  Auto)
  THEN  (GenConclAtAddrType  \mkleeneopen{}\mexists{}x:T.  \mexists{}L':T  List.  (l  =  (L'  @  [x]))\mkleeneclose{}  [2;1]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  Reduce  0
  THEN  Auto)

---

Home Index