---

Step * of Lemma decide-ite

∀[b:𝔹]. ∀[x,y,f,g:Top].
  (case if b then x else y fi  of inl(a) => f[a] | inr(a) => g[a] ~ if b
  then case x of inl(a) => f[a] | inr(a) => g[a]
  else case y of inl(a) => f[a] | inr(a) => g[a]
  fi )
BY
{ ((D 0 THENA Auto) THEN AutoBoolCase ⌜b⌝⋅) }

---

Latex:

---

Latex:
\mforall{}[b:\mBbbB{}].  \mforall{}[x,y,f,g:Top].
    (case  if  b  then  x  else  y  fi    of  inl(a)  =>  f[a]  |  inr(a)  =>  g[a]  \msim{}  if  b
    then  case  x  of  inl(a)  =>  f[a]  |  inr(a)  =>  g[a]
    else  case  y  of  inl(a)  =>  f[a]  |  inr(a)  =>  g[a]
    fi  )


By

---

Latex:
((D  0  THENA  Auto)  THEN  AutoBoolCase  \mkleeneopen{}b\mkleeneclose{}\mcdot{})

---

Home Index