Nuprl Lemma : length_of_null_list
∀[A:Type]. ∀[as:A List]. ||as|| = 0 ∈ ℤ supposing as = [] ∈ (A List)
Proof
Definitions occuring in Statement :
length: ||as||,
nil: [],
list: T List,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
natural_number: $n,
int: ℤ,
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
prop: ℙ
Lemmas referenced :
length_of_nil_lemma,
equal-wf-T-base,
length_wf,
list_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
introduction,
cut,
hypothesis,
thin,
sqequalRule,
extract_by_obid,
natural_numberEquality,
hyp_replacement,
equalitySymmetry,
applyLambdaEquality,
sqequalHypSubstitution,
isectElimination,
intEquality,
hypothesisEquality,
baseClosed,
Error :universeIsType,
isect_memberEquality,
axiomEquality,
because_Cache,
equalityTransitivity,
universeEquality
Latex:
\mforall{}[A:Type]. \mforall{}[as:A List]. ||as|| = 0 supposing as = []
Date html generated:
2019_06_20-PM-00_39_53
Last ObjectModification:
2018_09_26-PM-02_12_29
Theory : list_0
Home
Index