Nuprl Lemma : list-cases2
∀[T:Type]. ∀x:T List. ((x ~ []) ∨ (x ~ [hd(x) / tl(x)]))
Proof
Definitions occuring in Statement :
tl: tl(l),
hd: hd(l),
cons: [a / b],
nil: [],
list: T List,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
or: P ∨ Q,
universe: Type,
sqequal: s ~ t
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
member: t ∈ T,
or: P ∨ Q,
cons: [a / b],
top: Top,
squash: ↓T,
prop: ℙ,
true: True,
uimplies: b supposing a,
guard: {T},
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
implies: P ⇒ Q
Lemmas referenced :
list-cases,
istype-sqequal,
product_subtype_list,
reduce_hd_cons_lemma,
istype-void,
reduce_tl_cons_lemma,
list_wf,
istype-universe,
istype_wf,
squash_wf,
true_wf,
not-cons-sq-nil,
iff_weakening_equal
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
Error :lambdaFormation_alt,
cut,
hypothesisEquality,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesis,
dependent_functionElimination,
unionElimination,
Error :inlFormation_alt,
baseClosed,
promote_hyp,
hypothesis_subsumption,
productElimination,
sqequalRule,
Error :isect_memberEquality_alt,
voidElimination,
Error :inrFormation_alt,
Error :universeIsType,
instantiate,
universeEquality,
applyEquality,
Error :lambdaEquality_alt,
imageElimination,
equalityTransitivity,
equalitySymmetry,
natural_numberEquality,
imageMemberEquality,
independent_isectElimination,
independent_functionElimination
Latex:
\mforall{}[T:Type]. \mforall{}x:T List. ((x \msim{} []) \mvee{} (x \msim{} [hd(x) / tl(x)]))
Date html generated:
2019_06_20-PM-00_38_38
Last ObjectModification:
2018_10_18-PM-01_26_32
Theory : list_0
Home
Index