---

Step * of Lemma es-decl-sets-compatible_wf

∀[dd1,dd2:DeclSet].  (dd1 || dd2 ∈ ℙ')
BY
{ Auto }

---

Latex:


\mforall{}[dd1,dd2:DeclSet].    (dd1  ||  dd2  \mmember{}  \mBbbP{}')


By

Auto

---

Home Index