Nuprl Lemma : not_id_sqle_bottom
¬(λx.x ≤ ⊥)
Proof
Definitions occuring in Statement :
bottom: ⊥,
not: ¬A,
lambda: λx.A[x],
sqle: s ≤ t
Lemmas referenced :
not_id_sqeq_bottom,
not-id-sqle-bottom
Rules used in proof :
cut,
introduction,
extract_by_obid,
hypothesis
Latex:
\mneg{}(\mlambda{}x.x \mleq{} \mbot{})
Date html generated:
2018_05_21-PM-00_02_23
Last ObjectModification:
2018_05_01-PM-03_44_59
Theory : call!by!value_2
Home
Index