---

Step * of Lemma fpf-dom_wf

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[f:a:A fp-> Top]. ∀[x:A].  (x ∈ dom(f) ∈ 𝔹)
BY
{ (Unfolds ``fpf fpf-dom`` 0 THEN Auto) }

---

Latex:


\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[f:a:A  fp->  Top].  \mforall{}[x:A].    (x  \mmember{}  dom(f)  \mmember{}  \mBbbB{})


By

(Unfolds  ``fpf  fpf-dom``  0  THEN  Auto)

---

Home Index