---

Step * of Lemma test-decide-normalize

∀[a,B:Top].
  (case a of inl(_) => a + 1 | inr(y) => B[y] + a ~ case a of inl(x) => (inl x) + 1 | inr(y) => B[y] + (inr y ))
BY
{ (NormalizeDecide 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,B:Top].
    (case  a  of  inl($_{}$)  =>  a  +  1  |  inr(y)  =>  B[y]  +  a  \msim{}  case  a
      of  inl(x)  =>
      (inl  x)  +  1
      |  inr(y)  =>
      B[y]  +  (inr  y  ))


By

---

Latex:
(NormalizeDecide  0  THEN  Auto)

---

Home Index