---

Step * of Lemma normalize-decide-right

∀[a,F,G:Top].  (case a of inl(x) => F[x] | inr(x) => G[x] a ~ case a of inl(x) => F[x] | inr(x) => G[x] (inr x ))
BY
{ SqReasoning }

---

Latex:

---

Latex:
\mforall{}[a,F,G:Top].
    (case  a  of  inl(x)  =>  F[x]  |  inr(x)  =>  G[x]  a  \msim{}  case  a  of  inl(x)  =>  F[x]  |  inr(x)  =>  G[x]  (inr  x  ))


By

---

Latex:
SqReasoning

---

Home Index