---

Step * of Lemma fan-iff-dfan-bool

Fan ⇐⇒ Fan
BY
{ (Unfolds ``fan dfan`` 0
   THEN Folds ``tbar ubar dec-predicate`` 0
   THEN Unfold `dbar` 0
   THEN Auto
   THEN BackThruSomeHyp
   THEN Auto) }

---

Latex:

---

Latex:
Fan  \mLeftarrow{}{}\mRightarrow{}  Fan


By

---

Latex:
(Unfolds  ``fan  dfan``  0
  THEN  Folds  ``tbar  ubar  dec-predicate``  0
  THEN  Unfold  `dbar`  0
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index