Step
*
1
1
of Lemma
not_id_sqeq_bottom
1. λx.x ~ ⊥@i
2. λx.x ≤ ⊥
3. ⊥ ≤ λx.x
⊢ False
BY
{ (InstLemma `not-id-sqle-bottom` [] THEN Auto) }
Latex:
Latex:
1. \mlambda{}x.x \msim{} \mbot{}@i
2. \mlambda{}x.x \mleq{} \mbot{}
3. \mbot{} \mleq{} \mlambda{}x.x
\mvdash{} False
By
Latex:
(InstLemma `not-id-sqle-bottom` [] THEN Auto)
Home
Index