---

Step * of Lemma decide-append

∀[d,F,G,L:Top].  (case d of inl(x) => F[x] | inr(y) => G[y] @ L ~ case d of inl(x) => F[x] @ L | inr(y) => G[y] @ L)
BY
{ (Auto THEN RepUR ``append list_ind cons so_apply`` 0 THEN UnrollLoopsOnce) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  RepUR  ``append  list\_ind  cons  so\_apply``  0  THEN  UnrollLoopsOnce)

---

Home Index