---

Step * of Lemma name_eq-normalize3

∀[F,G,X,a,b:Top].
  (case name_eq(a;b) ∧b X of inl(x) => F[a] | inr(y) => G ~ case name_eq(a;b) ∧b X of inl(x) => F[b] | inr(y) => G)
BY
{ ((UnivCD THENA Auto) THEN RepUR ``so_apply`` 0 THEN BLemma `name_eq-normalize2` THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepUR  ``so\_apply``  0  THEN  BLemma  `name\_eq-normalize2`  THEN  Auto)

---

Home Index