---

Step * of Lemma map-decide

∀[b,f,L1,L2:Top].
  (map(f;case b of inl(a) => L1[a] | inr(a) => L2[a]) ~ case b of inl(a) => map(f;L1[a]) | inr(a) => map(f;L2[a]))
BY
{ ((UnivCD THENA Auto) THEN RepUR ``map list_ind`` 0 THEN RW UnrollLoopsOnceC 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[b,f,L1,L2:Top].
    (map(f;case  b  of  inl(a)  =>  L1[a]  |  inr(a)  =>  L2[a])  \msim{}  case  b
      of  inl(a)  =>
      map(f;L1[a])
      |  inr(a)  =>
      map(f;L2[a]))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepUR  ``map  list\_ind``  0  THEN  RW  UnrollLoopsOnceC  0  THEN  Auto)

---

Home Index