---

Step * 1 of Lemma provisional-type-wf2


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

---

Latex:

---

Latex:

1.  T  :  \mBbbU{}''
\mvdash{}  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:
((D  0  THEN  Auto)
  THEN  D  0
  THEN  Reduce  0
  THEN  Intros
  THEN  Try  (DProdsAndUnions)
  THEN  All  Reduce
  THEN  Auto)

---

Home Index