---

Step * of Lemma allow_wf

No Annotations
∀[T:𝕌']. ∀[x:Provisional(T)].  allow(x) ∈ T supposing allowed(x)
BY
{ ((Auto THEN D 2) THEN Unfold `allow` 0 THEN ExRepD THEN Unfold `allowed` -1 THEN UsquashElim (-1) THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  D  2)
  THEN  Unfold  `allow`  0
  THEN  ExRepD
  THEN  Unfold  `allowed`  -1
  THEN  UsquashElim  (-1)
  THEN  Auto)

---

Home Index