---

Step * of Lemma allowed-trivial-iff

No Annotations
∀[T:𝕌']. ∀[x:Provisional(T)]. ∀[X:ℙ].  (SqStable(X) ⇒ allowed(x) ⇐⇒ usquash(allowed(x) ∧ X) supposing X)
BY
{ Auto }

1
1. [T] : 𝕌'
2. [x] : Provisional(T)
3. [X] : ℙ
4. SqStable(X)
5. [%1] : X
6. allowed(x)
⊢ usquash(allowed(x) ∧ X)

2
1. [T] : 𝕌'
2. [x] : Provisional(T)
3. [X] : ℙ
4. SqStable(X)
5. [%1] : X
6. usquash(allowed(x) ∧ X)
⊢ allowed(x)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:\mBbbU{}'].  \mforall{}[x:Provisional(T)].  \mforall{}[X:\mBbbP{}].
    (SqStable(X)  {}\mRightarrow{}  allowed(x)  \mLeftarrow{}{}\mRightarrow{}  usquash(allowed(x)  \mwedge{}  X)  supposing  X)


By

---

Latex:
Auto

---

Home Index