---

Step * of Lemma lifting-callbyvalueall-decide-name_eq

∀[a,b,F,G,H:Top].
  (let x ⟵ case name_eq(a;b) of inl(x) => F[x] | inr(x) => H[x]
   in G[x] ~ case name_eq(a;b) of inl(x) => let x ⟵ F[x] in G[x] | inr(x) => let x ⟵ H[x] in G[x])
BY
{ (RWO "lifting-callbyvalueall-decide" 0 THEN Auto) }

---

Latex:

---

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


By

---

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

---

Home Index