---

Step * 1 of Lemma ispair-or-isaxiom-append-nil


1. l : Base@i
2. (l @ [])↓@i
3. ∀a,b:Top.  (if l @ [] is a pair then a otherwise b ~ b)
4. ∀a,b:Top.  (if l @ [] = Ax then a otherwise b ~ b)
⊢ False
BY
{ (RepeatFor 2 ((InstHyp [⌜tt⌝;⌜ff⌝] (-2)⋅ THENA Auto))
   THEN RepeatFor 2 (Thin (-3))
   THEN (All (RWO "sqeqff_to_assert")⋅ THENA CanonicalAuto)
   THEN (All (RW assert_pushdownC) THENA CanonicalAuto)
   THEN All (RepUR ``append list_ind``)
   THEN All(RW UnrollLoopsC)
   THEN AllReduce
   THEN HasValueD (-3)
   THEN HVimplies2 (-4) [1]⋅
   THEN HVimplies2 (-5) [1]⋅
   THEN BotDiv) }

---

Latex:

---

Latex:

1.  l  :  Base@i
2.  (l  @  [])\mdownarrow{}@i
3.  \mforall{}a,b:Top.    (if  l  @  []  is  a  pair  then  a  otherwise  b  \msim{}  b)
4.  \mforall{}a,b:Top.    (if  l  @  []  =  Ax  then  a  otherwise  b  \msim{}  b)
\mvdash{}  False


By

---

Latex:
(RepeatFor  2  ((InstHyp  [\mkleeneopen{}tt\mkleeneclose{};\mkleeneopen{}ff\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto))
  THEN  RepeatFor  2  (Thin  (-3))
  THEN  (All  (RWO  "sqeqff\_to\_assert")\mcdot{}  THENA  CanonicalAuto)
  THEN  (All  (RW  assert\_pushdownC)  THENA  CanonicalAuto)
  THEN  All  (RepUR  ``append  list\_ind``)
  THEN  All(RW  UnrollLoopsC)
  THEN  AllReduce
  THEN  HasValueD  (-3)
  THEN  HVimplies2  (-4)  [1]\mcdot{}
  THEN  HVimplies2  (-5)  [1]\mcdot{}
  THEN  BotDiv)

---

Home Index