---

Step * of Lemma ds-agrees-on_wf

∀[ds:x:Id fp-> Type]. ∀[x:Id]. ∀[T:Type].  (ds-agrees-on(ds;x;T) ∈ ℙ)
BY
{ (Unfold `ds-agrees-on` 0 THEN Auto) }

---

Latex:


\mforall{}[ds:x:Id  fp->  Type].  \mforall{}[x:Id].  \mforall{}[T:Type].    (ds-agrees-on(ds;x;T)  \mmember{}  \mBbbP{})


By

(Unfold  `ds-agrees-on`  0  THEN  Auto)

---

Home Index