---

Step * 1 1 of Lemma peval_wf

.....set predicate..... 
1. x : formula()
2. v0 : {a:formula()| a ⊆ x ∧ (↑pvar?(a))}  ⟶ 𝔹
⊢ x ⊆ x
BY
{ (BLemma `psub_weakening` THEN Auto)⋅ }

---

Latex:

---

Latex:
.....set  predicate..... 
1.  x  :  formula()
2.  v0  :  \{a:formula()|  a  \msubseteq{}  x  \mwedge{}  (\muparrow{}pvar?(a))\}    {}\mrightarrow{}  \mBbbB{}
\mvdash{}  x  \msubseteq{}  x


By

---

Latex:
(BLemma  `psub\_weakening`  THEN  Auto)\mcdot{}

---

Home Index