Step
*
of Lemma
no-value-bottom-base
∀[x:Base]. x ~ ⊥ supposing (¬(x)↓) ∧ (¬is-exception(x))
BY
{ (SqReasoning THEN Try ((InstLemma `is-exception_wf` [⌜x⌝]⋅ THEN Auto))) }
Latex:
Latex:
\mforall{}[x:Base]. x \msim{} \mbot{} supposing (\mneg{}(x)\mdownarrow{}) \mwedge{} (\mneg{}is-exception(x))
By
Latex:
(SqReasoning THEN Try ((InstLemma `is-exception\_wf` [\mkleeneopen{}x\mkleeneclose{}]\mcdot{} THEN Auto)))
Home
Index