---

Step * of Lemma is-strict-fun

∀[f:Base]. f ∈ StrictFun supposing f ⊥ ~ ⊥
BY
{ (InstLemma `strict-fun` [] THEN Fold `strict-fun` (-1) THEN Hypothesis) }

---

Latex:

---

Latex:
\mforall{}[f:Base].  f  \mmember{}  StrictFun  supposing  f  \mbot{}  \msim{}  \mbot{}


By

---

Latex:
(InstLemma  `strict-fun`  []  THEN  Fold  `strict-fun`  (-1)  THEN  Hypothesis)

---

Home Index