---

Step * 2 of Lemma allowed-trivial-iff


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

---

Latex:

---

Latex:

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


By

---

Latex:
(FLemma  `usquash-elim`  [-1]  THEN  Auto)

---

Home Index