---

Step * of Lemma apply-strict-fun

∀[f:StrictFun]. (f ⊥ ~ ⊥)
BY
{ (Auto THEN Unfold `strict-fun` 1 THEN BLemma `partial-void` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[f:StrictFun].  (f  \mbot{}  \msim{}  \mbot{})


By

---

Latex:
(Auto  THEN  Unfold  `strict-fun`  1  THEN  BLemma  `partial-void`  THEN  Auto)

---

Home Index