---

Step * of Lemma provisional-type-wf2

No Annotations
∀[T:𝕌'']. (Provisional(T) ∈ 𝕌'')
BY
{ ProveWfLemma }

1
1. T : 𝕌''
⊢ EquivRel(ok:ℙ × T supposing ↓ok;x,y.(↓fst(x) ⇐⇒ ↓fst(y)) ∧ ((↓fst(x)) ⇒ ((snd(x)) = (snd(y)) ∈ T)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:\mBbbU{}''].  (Provisional(T)  \mmember{}  \mBbbU{}'')


By

---

Latex:
ProveWfLemma

---

Home Index