---

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

∀[l:Base]. (fst((l @ [])) ~ fst(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) }

---

Latex:

---

Latex:
\mforall{}[l:Base].  (fst((l  @  []))  \msim{}  fst(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)

---

Home Index