Nuprl Lemma : dl-conj_wf
∀[L:Prop List]. (dl-conj(L) ∈ Prop)
Proof
Definitions occuring in Statement :
dl-conj: dl-conj(L),
dl-prop: Prop,
list: T List,
uall: ∀[x:A]. B[x],
member: t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
dl-conj: dl-conj(L)
Lemmas referenced :
reduce_wf,
dl-prop_wf,
dl-and_wf,
dl-true_wf,
list_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
sqequalRule,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesis,
lambdaEquality_alt,
hypothesisEquality,
inhabitedIsType,
universeIsType,
axiomEquality,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}[L:Prop List]. (dl-conj(L) \mmember{} Prop)
Date html generated:
2019_10_15-AM-11_45_46
Last ObjectModification:
2019_05_06-PM-04_44_19
Theory : dynamic!logic
Home
Index