Nuprl Lemma : before_wf
∀a:DSet. ∀ps:|a| List. ∀u:|a|. (before(u;ps) ∈ 𝔹)
Proof
Definitions occuring in Statement :
before: before(u;ps),
list: T List,
bool: 𝔹,
all: ∀x:A. B[x],
member: t ∈ T,
dset: DSet,
set_car: |p|
Definitions unfolded in proof :
before: before(u;ps),
all: ∀x:A. B[x],
member: t ∈ T,
uall: ∀[x:A]. B[x],
dset: DSet,
or: P ∨ Q,
btrue: tt,
bor: p ∨bq,
ifthenelse: if b then t else f fi ,
cons: [a / b],
top: Top,
bfalse: ff
Lemmas referenced :
set_car_wf,
list_wf,
dset_wf,
list-cases,
null_nil_lemma,
btrue_wf,
product_subtype_list,
null_cons_lemma,
istype-void,
reduce_hd_cons_lemma,
set_blt_wf
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lambdaFormation_alt,
cut,
sqequalHypSubstitution,
hypothesis,
universeIsType,
introduction,
extract_by_obid,
isectElimination,
thin,
setElimination,
rename,
hypothesisEquality,
dependent_functionElimination,
unionElimination,
promote_hyp,
hypothesis_subsumption,
productElimination,
isect_memberEquality_alt,
voidElimination
Latex:
\mforall{}a:DSet. \mforall{}ps:|a| List. \mforall{}u:|a|. (before(u;ps) \mmember{} \mBbbB{})
Date html generated:
2019_10_16-PM-01_07_00
Last ObjectModification:
2018_10_08-PM-00_42_05
Theory : polynom_2
Home
Index