Nuprl Lemma : colength-cons-not-zero
∀[T:Type]. ∀[v:T List]. ∀[u:Top]. False supposing colength([u / v]) = 0 ∈ ℕ
Proof
Definitions occuring in Statement :
cons: [a / b],
list: T List,
colength: colength(L),
nat: ℕ,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
top: Top,
false: False,
natural_number: $n,
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
colength: colength(L),
cons: [a / b],
uimplies: b supposing a,
member: t ∈ T,
false: False,
all: ∀x:A. B[x],
implies: P ⇒ Q,
nat: ℕ,
squash: ↓T,
sq_stable: SqStable(P),
uiff: uiff(P;Q),
and: P ∧ Q,
guard: {T},
subtype_rel: A ⊆r B,
top: Top,
le: A ≤ B,
not: ¬A,
less_than': less_than'(a;b),
true: True
Lemmas referenced :
istype-top,
list_wf,
colength_wf_list,
sq_stable__le,
le_antisymmetry_iff,
add_functionality_wrt_le,
add-associates,
istype-void,
istype-int,
add-zero,
zero-add,
le-add-cancel,
int_subtype_base
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
sqequalRule,
introduction,
cut,
sqequalHypSubstitution,
voidElimination,
extract_by_obid,
hypothesis,
Error :universeIsType,
isectElimination,
thin,
hypothesisEquality,
universeEquality,
Error :inhabitedIsType,
Error :lambdaFormation_alt,
applyLambdaEquality,
setElimination,
rename,
imageMemberEquality,
baseClosed,
natural_numberEquality,
independent_functionElimination,
imageElimination,
addEquality,
productElimination,
independent_isectElimination,
applyEquality,
Error :lambdaEquality_alt,
Error :isect_memberEquality_alt,
because_Cache,
Error :equalityIsType4,
Error :equalityIsType1,
equalityTransitivity,
equalitySymmetry,
dependent_functionElimination
Latex:
\mforall{}[T:Type]. \mforall{}[v:T List]. \mforall{}[u:Top]. False supposing colength([u / v]) = 0
Date html generated:
2019_06_20-PM-00_38_15
Last ObjectModification:
2018_10_03-PM-09_54_43
Theory : list_0
Home
Index