---

Step * of Lemma band-simple-decide

∀[a,b:Top].  (case a of inl(y) => inl ⋅ | inr(z) => inr ⋅  ∧b b ~ case a of inl(y) => b | inr(z) => inr ⋅ )
BY
{ (RW (BasicSymbolicComputeC []) 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,b:Top].
    (case  a  of  inl(y)  =>  inl  \mcdot{}  |  inr(z)  =>  inr  \mcdot{}    \mwedge{}\msubb{}  b  \msim{}  case  a  of  inl(y)  =>  b  |  inr(z)  =>  inr  \mcdot{}  )


By

---

Latex:
(RW  (BasicSymbolicComputeC  [])  0  THEN  Auto)

---

Home Index