---

Step * of Lemma pi2-if-ispair-append-nil

∀[l:Base]. (snd((l @ [])) ~ (snd(l)) @ []) supposing ((↑ispair(l @ [])) and (l @ [])↓)
BY
{ (Repeat (Intro)
   THEN Try (Complete ((UniverseIsType THEN EqCD THEN CanonicalAuto)))
   THEN SqUnhide⋅
   THEN All(RepUR ``append list_ind``)
   THEN RW UnrollLoopsC (-1)
   THEN RW UnrollLoopsC (-2)
   THEN RW UnrollLoopsC 0
   THEN AllReduce
   THEN HasValueD (-2)
   THEN Repeat ((HVimplies2 0 [1;1] THEN Try (Complete ((RepUR ``cons`` 0 THEN Auto)))))
   THEN BotDiv
   THEN RepUR ``cons`` 0
   THEN RW (AddrC [1] UnrollLoopsC) 0
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[l:Base].  (snd((l  @  []))  \msim{}  (snd(l))  @  [])  supposing  ((\muparrow{}ispair(l  @  []))  and  (l  @  [])\mdownarrow{})


By

---

Latex:
(Repeat  (Intro)
  THEN  Try  (Complete  ((UniverseIsType  THEN  EqCD  THEN  CanonicalAuto)))
  THEN  SqUnhide\mcdot{}
  THEN  All(RepUR  ``append  list\_ind``)
  THEN  RW  UnrollLoopsC  (-1)
  THEN  RW  UnrollLoopsC  (-2)
  THEN  RW  UnrollLoopsC  0
  THEN  AllReduce
  THEN  HasValueD  (-2)
  THEN  Repeat  ((HVimplies2  0  [1;1]  THEN  Try  (Complete  ((RepUR  ``cons``  0  THEN  Auto)))))
  THEN  BotDiv
  THEN  RepUR  ``cons``  0
  THEN  RW  (AddrC  [1]  UnrollLoopsC)  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index