---

Step * of Lemma lifting-bag-combine-decide-name_eq

∀[a,b,F,G,f:Top].
  (⋃b∈case name_eq(a;b) of inl(x) => F[x] | inr(x) => G[x].f[b] ~ case name_eq(a;b)
   of inl(x) =>
   ⋃b∈F[x].f[b]
   | inr(x) =>
   ⋃b∈G[x].f[b])
BY
{ (RWO "lifting-bag-combine-decide" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,b,F,G,f:Top].
    (\mcup{}b\mmember{}case  name\_eq(a;b)  of  inl(x)  =>  F[x]  |  inr(x)  =>  G[x].f[b]  \msim{}  case  name\_eq(a;b)
      of  inl(x)  =>
      \mcup{}b\mmember{}F[x].f[b]
      |  inr(x)  =>
      \mcup{}b\mmember{}G[x].f[b])


By

---

Latex:
(RWO  "lifting-bag-combine-decide"  0  THEN  Auto)

---

Home Index