Nuprl Lemma : sub-bags_wf

[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)].  (sub-bags(eq;bs) ∈ bag(bag(T))) supposing valueall-type(T)


Proof




Definitions occuring in Statement :  sub-bags: sub-bags(eq;bs) bag: bag(T) deq: EqDecider(T) valueall-type: valueall-type(T) uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a sub-bags: sub-bags(eq;bs) subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] all: x:A. B[x] top: Top
Lemmas referenced :  bag-map_wf bag_wf pi1_wf_top subtype_rel_product top_wf bag-partitions_wf deq_wf valueall-type_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis productEquality lambdaEquality applyEquality because_Cache independent_isectElimination lambdaFormation isect_memberEquality voidElimination voidEquality axiomEquality equalityTransitivity equalitySymmetry universeEquality

Latex:
\mforall{}[T:Type]
    \mforall{}[eq:EqDecider(T)].  \mforall{}[bs:bag(T)].    (sub-bags(eq;bs)  \mmember{}  bag(bag(T)))  supposing  valueall-type(T)



Date html generated: 2016_05_15-PM-08_09_44
Last ObjectModification: 2015_12_27-PM-04_12_28

Theory : bags_2


Home Index