Nuprl Lemma : bag-to-set_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)].  (bag-to-set(eq;bs) ∈ bag(T))
Proof
Definitions occuring in Statement : 
bag-to-set: bag-to-set(eq;bs)
, 
bag: bag(T)
, 
deq: EqDecider(T)
, 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
universe: Type
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
bag-to-set: bag-to-set(eq;bs)
Lemmas referenced : 
bag-remove-repeats_wf, 
bag_wf, 
deq_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation, 
introduction, 
cut, 
sqequalRule, 
lemma_by_obid, 
sqequalHypSubstitution, 
isectElimination, 
thin, 
hypothesisEquality, 
hypothesis, 
axiomEquality, 
equalityTransitivity, 
equalitySymmetry, 
isect_memberEquality, 
because_Cache, 
universeEquality
Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[bs:bag(T)].    (bag-to-set(eq;bs)  \mmember{}  bag(T))
Date html generated:
2016_05_15-PM-08_03_00
Last ObjectModification:
2015_12_27-PM-04_15_33
Theory : bags_2
Home
Index