---

Step * of Lemma is-list-if-has-value-rec-pair-bot

∀[t:Base]. is-list-if-has-value-rec(<t, ⊥>)
BY
{ (Auto
   THEN RepUR ``is-list-if-has-value-rec is-list-if-has-value-fun`` 0
   THEN Auto
   THEN UseWitness ⌜Ax⌝⋅
   THEN RepeatFor 2 (((RWO "primrec-unroll" 0 THENA Auto) THEN AutoSplit THEN Try (Complete (Auto))))
   THEN Strictness
   THEN RepUR ``uimplies`` 0
   THEN MemTypeCD
   THEN Auto
   THEN BotDiv) }

---

Latex:

---

Latex:
\mforall{}[t:Base].  is-list-if-has-value-rec(<t,  \mbot{}>)


By

---

Latex:
(Auto
  THEN  RepUR  ``is-list-if-has-value-rec  is-list-if-has-value-fun``  0
  THEN  Auto
  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
  THEN  RepeatFor  2  (((RWO  "primrec-unroll"  0  THENA  Auto)  THEN  AutoSplit  THEN  Try  (Complete  (Auto))))
  THEN  Strictness
  THEN  RepUR  ``uimplies``  0
  THEN  MemTypeCD
  THEN  Auto
  THEN  BotDiv)

---

Home Index