Nuprl Lemma : single-valued-bag-list

`∀[T:Type]. ∀[L:T List].  single-valued-list(L;T) supposing single-valued-bag(L;T)`

Proof

Definitions occuring in Statement :  single-valued-bag: `single-valued-bag(b;T)` single-valued-list: `single-valued-list(L;T)` list: `T List` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` single-valued-bag: `single-valued-bag(b;T)` single-valued-list: `single-valued-list(L;T)` all: `∀x:A. B[x]` implies: `P `` Q` prop: `ℙ` subtype_rel: `A ⊆r B`
Lemmas referenced :  list-member-bag-member l_member_wf single-valued-bag_wf list-subtype-bag list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution lambdaFormation hypothesis dependent_functionElimination thin hypothesisEquality independent_functionElimination lemma_by_obid isectElimination because_Cache sqequalRule lambdaEquality axiomEquality applyEquality independent_isectElimination isect_memberEquality equalityTransitivity equalitySymmetry universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].    single-valued-list(L;T)  supposing  single-valued-bag(L;T)

Date html generated: 2016_05_15-PM-02_42_58
Last ObjectModification: 2015_12_27-AM-09_39_15

Theory : bags

Home Index