Nuprl Lemma : single-bag_wf

T:Type. ∀x:T.  ({x} ∈ bag(T))


Proof




Definitions occuring in Statement :  single-bag: {x} bag: bag(T) all: x:A. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T single-bag: {x} uall: [x:A]. B[x] subtype_rel: A ⊆B uimplies: supposing a
Lemmas referenced :  cons_wf nil_wf list-subtype-bag
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality because_Cache hypothesis applyEquality independent_isectElimination lambdaEquality universeEquality

Latex:
\mforall{}T:Type.  \mforall{}x:T.    (\{x\}  \mmember{}  bag(T))



Date html generated: 2016_05_15-PM-02_21_48
Last ObjectModification: 2015_12_27-AM-09_55_19

Theory : bags


Home Index