---

Step * 1 of Lemma allowed-trivial-iff


1. [T] : 𝕌'
2. [x] : Provisional(T)
3. [X] : ℙ
4. SqStable(X)
5. [%1] : X
6. allowed(x)
⊢ usquash(allowed(x) ∧ X)
BY
{ (BLemma `squash-implies-usquash` THEN Auto THEN Unhide THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  \mBbbU{}'
2.  [x]  :  Provisional(T)
3.  [X]  :  \mBbbP{}
4.  SqStable(X)
5.  [\%1]  :  X
6.  allowed(x)
\mvdash{}  usquash(allowed(x)  \mwedge{}  X)


By

---

Latex:
(BLemma  `squash-implies-usquash`  THEN  Auto  THEN  Unhide  THEN  Auto)

---

Home Index