---

Step * of Lemma strict-fun

∀[f:Base]. f ∈ partial(Void) ⟶ partial(Void) supposing f ⊥ ~ ⊥
BY
{ (Auto
   THEN FunExt
   THEN Auto
   THEN (Subst' x ~ ⊥ 0 THENA (BLemma `partial-void` THEN Auto))
   THEN HypSubst' 2 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[f:Base].  f  \mmember{}  partial(Void)  {}\mrightarrow{}  partial(Void)  supposing  f  \mbot{}  \msim{}  \mbot{}


By

---

Latex:
(Auto
  THEN  FunExt
  THEN  Auto
  THEN  (Subst'  x  \msim{}  \mbot{}  0  THENA  (BLemma  `partial-void`  THEN  Auto))
  THEN  HypSubst'  2  0
  THEN  Auto)

---

Home Index