---

Step * of Lemma provisional-equiv

No Annotations
∀[T:𝕌']. EquivRel(ok:ℙ × T supposing ↓ok;x,y.(↓fst(x) ⇐⇒ ↓fst(y)) ∧ ((↓fst(x)) ⇒ ((snd(x)) = (snd(y)) ∈ T)))
BY
{ (Auto THEN (D 0 THEN Auto) THEN D 0 THEN Reduce 0 THEN Intros THEN Try (DProdsAndUnions) THEN All Reduce THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:\mBbbU{}']
    EquivRel(ok:\mBbbP{}  \mtimes{}  T  supposing  \mdownarrow{}ok;x,y.(\mdownarrow{}fst(x)  \mLeftarrow{}{}\mRightarrow{}  \mdownarrow{}fst(y))  \mwedge{}  ((\mdownarrow{}fst(x))  {}\mRightarrow{}  ((snd(x))  =  (snd(y)))))


By

---

Latex:
(Auto
  THEN  (D  0  THEN  Auto)
  THEN  D  0
  THEN  Reduce  0
  THEN  Intros
  THEN  Try  (DProdsAndUnions)
  THEN  All  Reduce
  THEN  Auto)

---

Home Index