---

Step * of Lemma equality-test2

∀[A,B,C:Type].
  ((A = B ∈ Type)
  ⇒ (C = B ∈ Type)
  ⇒ (∀[f:A ⟶ A]. ∀[x,y,z,u,w:A].  ((x = (f y) ∈ A) ⇒ (z = (f y) ∈ A) ⇒ (w = u ∈ C) ⇒ (w = z ∈ C) ⇒ (u = x ∈ C))))
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].
    ((A  =  B)
    {}\mRightarrow{}  (C  =  B)
    {}\mRightarrow{}  (\mforall{}[f:A  {}\mrightarrow{}  A].  \mforall{}[x,y,z,u,w:A].    ((x  =  (f  y))  {}\mRightarrow{}  (z  =  (f  y))  {}\mRightarrow{}  (w  =  u)  {}\mRightarrow{}  (w  =  z)  {}\mRightarrow{}  (u  =  x))))


By

---

Latex:
Auto

---

Home Index