Nuprl Lemma : cons_before
∀[T:Type]. ∀l:T List. ∀a,x,y:T. (x before y ∈ [a / l] ⇐⇒ ((x = a ∈ T) ∧ (y ∈ l)) ∨ x before y ∈ l)
Proof
Definitions occuring in Statement :
l_before: x before y ∈ l,
l_member: (x ∈ l),
cons: [a / b],
list: T List,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
l_before: x before y ∈ l,
iff: P ⇐⇒ Q,
and: P ∧ Q,
implies: P ⇒ Q,
or: P ∨ Q,
member: t ∈ T,
prop: ℙ,
rev_implies: P ⇐ Q
Lemmas referenced :
sublist_wf,
cons_wf,
nil_wf,
cons_sublist_cons,
member_iff_sublist,
l_member_wf,
list_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
Error :lambdaFormation_alt,
cut,
independent_pairFormation,
hypothesis,
sqequalRule,
Error :unionIsType,
Error :productIsType,
Error :equalityIsType1,
Error :inhabitedIsType,
hypothesisEquality,
Error :universeIsType,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
because_Cache,
productElimination,
independent_functionElimination,
dependent_functionElimination,
promote_hyp,
unionElimination,
Error :inlFormation_alt,
Error :inrFormation_alt,
universeEquality
Latex:
\mforall{}[T:Type]. \mforall{}l:T List. \mforall{}a,x,y:T. (x before y \mmember{} [a / l] \mLeftarrow{}{}\mRightarrow{} ((x = a) \mwedge{} (y \mmember{} l)) \mvee{} x before y \mmember{} l)
Date html generated:
2019_06_20-PM-01_23_32
Last ObjectModification:
2018_09_29-PM-00_28_12
Theory : list_1
Home
Index