---

Step * of Lemma stuck-decide

∀[a:Base]
  (∀[F,H:Top].  (case a of inl(x) => F[x] | inr(x) => H[x] ~ eval x = a in ⊥)) supposing 
     ((∀b,c:Base.  (if a is inl then b else c ~ c)) and 
     (∀b,c:Base.  (if a is inr then b else c ~ c)))
BY
{ (SqReasoning
   THEN (All(InstHyp [⌜tt⌝;⌜ff⌝])⋅ THENA Auto)
   THEN ElimVar `a'⋅
   THEN AllReduce
   THEN InstLemma `not-btrue-sqeq-bfalse` []
   THEN D (-1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a:Base]
    (\mforall{}[F,H:Top].    (case  a  of  inl(x)  =>  F[x]  |  inr(x)  =>  H[x]  \msim{}  eval  x  =  a  in  \mbot{}))  supposing 
          ((\mforall{}b,c:Base.    (if  a  is  inl  then  b  else  c  \msim{}  c))  and 
          (\mforall{}b,c:Base.    (if  a  is  inr  then  b  else  c  \msim{}  c)))


By

---

Latex:
(SqReasoning
  THEN  (All(InstHyp  [\mkleeneopen{}tt\mkleeneclose{};\mkleeneopen{}ff\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  ElimVar  `a'\mcdot{}
  THEN  AllReduce
  THEN  InstLemma  `not-btrue-sqeq-bfalse`  []
  THEN  D  (-1)
  THEN  Auto)

---

Home Index