---

Step * of Lemma fun-equiv-rel

∀[X,A:Type]. ∀[E:A ⟶ A ⟶ ℙ].  (EquivRel(A;a,b.E[a;b]) ⇒ EquivRel(X ⟶ A;f,g.fun-equiv(X;a,b.E[a;b];f;g)))
BY
{ (Auto THEN D 0 THEN Auto THEN RepUR ``refl sym trans fun-equiv`` 0 THEN Auto THEN UseTrans ⌜b x⌝⋅) }

---

Latex:

---

Latex:
\mforall{}[X,A:Type].  \mforall{}[E:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].
    (EquivRel(A;a,b.E[a;b])  {}\mRightarrow{}  EquivRel(X  {}\mrightarrow{}  A;f,g.fun-equiv(X;a,b.E[a;b];f;g)))


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  RepUR  ``refl  sym  trans  fun-equiv``  0  THEN  Auto  THEN  UseTrans  \mkleeneopen{}b  x\mkleeneclose{}\mcdot{})

---

Home Index