---

Step * of Lemma normalize-decide-left

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

---

Latex:

---

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


By

---

Latex:
SqReasoning

---

Home Index