---

Step * of Lemma name_eq-normalize-name

∀[X,F,G:Top]. ∀[a,b:Name].
  (case name_eq(a;b) ∧b X of inl(x) => F[x;a] | inr(x) => G[x] ~ case name_eq(a;b) ∧b X
   of inl(x) =>
   F[x;b]
   | inr(x) =>
   G[x])
BY
{ ((UnivCD THENA Auto) THEN BoolCase ⌜name_eq(a;b)⌝⋅ THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  BoolCase  \mkleeneopen{}name\_eq(a;b)\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index