---

Step * of Lemma dl_KripkeStructure_wf

No Annotations
dl_KripkeStructure ∈ 𝕌'
BY
{ (((Unfold `dl_KripkeStructure` 0 THEN Unfold `worlds` 0) THEN RecordWf) THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
dl\_KripkeStructure  \mmember{}  \mBbbU{}'


By

---

Latex:
(((Unfold  `dl\_KripkeStructure`  0  THEN  Unfold  `worlds`  0)  THEN  RecordWf)  THEN  Auto)

---

Home Index