Step
*
of Lemma
not_id_sqle_bottom
¬(λx.x ≤ ⊥)
BY
{ (InstLemma `not_id_sqeq_bottom` [] THEN Auto) }
Latex:
Latex:
\mneg{}(\mlambda{}x.x  \mleq{}  \mbot{})
By
Latex:
(InstLemma  `not\_id\_sqeq\_bottom`  []  THEN  Auto)
Home
Index