Nuprl Lemma : not-cons-sq-nil
∀[u,v:Top]. (([u / v] ~ []) = (0 ~ 1) ∈ Type)
Proof
Definitions occuring in Statement :
cons: [a / b],
nil: [],
uall: ∀[x:A]. B[x],
top: Top,
natural_number: $n,
universe: Type,
sqequal: s ~ t,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
implies: P ⇒ Q,
not: ¬A,
cons: [a / b],
nil: [],
it: ⋅,
uimplies: b supposing a,
sq_type: SQType(T),
all: ∀x:A. B[x],
guard: {T},
true: True,
false: False
Lemmas referenced :
istype-top,
false-sqequal,
subtype_base_sq,
int_subtype_base
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
introduction,
cut,
pointwiseFunctionalityForEquality,
universeEquality,
hypothesis,
Error :inhabitedIsType,
hypothesisEquality,
sqequalRule,
sqequalHypSubstitution,
Error :isect_memberEquality_alt,
isectElimination,
thin,
axiomEquality,
extract_by_obid,
baseApply,
closedConclusion,
baseClosed,
independent_functionElimination,
Error :lambdaFormation_alt,
Error :universeIsType,
sqequalIntensionalEquality,
natural_numberEquality,
instantiate,
cumulativity,
intEquality,
independent_isectElimination,
dependent_functionElimination,
equalityTransitivity,
equalitySymmetry,
voidElimination
Latex:
\mforall{}[u,v:Top]. (([u / v] \msim{} []) = (0 \msim{} 1))
Date html generated:
2019_06_20-PM-00_38_22
Last ObjectModification:
2018_10_07-PM-01_00_21
Theory : list_0
Home
Index