---

Step * of Lemma fpf-is-empty_wf

∀[A:Type]. ∀[f:x:A fp-> Top].  (fpf-is-empty(f) ∈ 𝔹)
BY
{ (Auto THEN (D (-1)) THEN Unfold `fpf-is-empty` 0 THEN Reduce 0 THEN Auto) }

---

Latex:


\mforall{}[A:Type].  \mforall{}[f:x:A  fp->  Top].    (fpf-is-empty(f)  \mmember{}  \mBbbB{})


By

(Auto  THEN  (D  (-1))  THEN  Unfold  `fpf-is-empty`  0  THEN  Reduce  0  THEN  Auto)

---

Home Index