Nuprl Lemma : not-id-sqle-bottom
¬(λx.x ≤ ⊥)
Proof
Definitions occuring in Statement :
bottom: ⊥,
not: ¬A,
lambda: λx.A[x],
sqle: s ≤ t
Definitions unfolded in proof :
prop: ℙ,
uall: ∀[x:A]. B[x],
member: t ∈ T,
implies: P ⇒ Q,
not: ¬A,
top: Top,
uimplies: b supposing a,
sq_type: SQType(T),
all: ∀x:A. B[x],
guard: {T},
true: True,
false: False
Lemmas referenced :
sqle_wf_base,
bottom-sqle,
istype-void,
strictness-apply,
subtype_base_sq,
int_subtype_base
Rules used in proof :
hypothesis,
baseClosed,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
Error :universeIsType,
Error :lambdaFormation_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
sqequalSqle,
Error :isect_memberEquality_alt,
voidElimination,
sqequalRule,
natural_numberEquality,
instantiate,
cumulativity,
intEquality,
independent_isectElimination,
dependent_functionElimination,
equalityTransitivity,
equalitySymmetry,
independent_functionElimination
Latex:
\mneg{}(\mlambda{}x.x \mleq{} \mbot{})
Date html generated:
2019_06_20-AM-11_27_21
Last ObjectModification:
2018_10_15-PM-04_53_50
Theory : call!by!value_2
Home
Index