---

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

∀[l:Base]. (l ∈ Top × Top) supposing ((↑ispair(l @ [])) and (l @ [])↓)
BY
{ (Repeat (Intro)
   THEN Try (Complete ((UniverseIsType THEN EqCD THEN CanonicalAuto)))
   THEN Unhide⋅
   THEN All(RepUR ``append list_ind``)
   THEN RW UnrollLoopsC (-1)
   THEN Reduce (-1)
   THEN RW UnrollLoopsC (-2)
   THEN Reduce (-2)
   THEN HasValueD (-2)
   THEN HVimplies2 (-3) [1]
   THEN HVimplies2 (-4) [1]
   THEN BotDiv) }

---

Latex:

---

Latex:
\mforall{}[l:Base].  (l  \mmember{}  Top  \mtimes{}  Top)  supposing  ((\muparrow{}ispair(l  @  []))  and  (l  @  [])\mdownarrow{})


By

---

Latex:
(Repeat  (Intro)
  THEN  Try  (Complete  ((UniverseIsType  THEN  EqCD  THEN  CanonicalAuto)))
  THEN  Unhide\mcdot{}
  THEN  All(RepUR  ``append  list\_ind``)
  THEN  RW  UnrollLoopsC  (-1)
  THEN  Reduce  (-1)
  THEN  RW  UnrollLoopsC  (-2)
  THEN  Reduce  (-2)
  THEN  HasValueD  (-2)
  THEN  HVimplies2  (-3)  [1]
  THEN  HVimplies2  (-4)  [1]
  THEN  BotDiv)

---

Home Index