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