---

Step * of Lemma provision_wf

No Annotations
∀[T:𝕌']. ∀[ok:ℙ]. ∀[v:T supposing ok].  (provision(ok; v) ∈ Provisional(T))
BY
{ (ProveWfLemma THEN Unfold `provisional-type` 0 THEN (Unfold `member` 0 THEN QuotientEqTypeCDUp) THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:\mBbbU{}'].  \mforall{}[ok:\mBbbP{}].  \mforall{}[v:T  supposing  ok].    (provision(ok;  v)  \mmember{}  Provisional(T))


By

---

Latex:
(ProveWfLemma
  THEN  Unfold  `provisional-type`  0
  THEN  (Unfold  `member`  0  THEN  QuotientEqTypeCDUp)
  THEN  Auto)

---

Home Index