Nuprl Lemma : bag_to_squash_list

[T:Type]. ∀[b:bag(T)].  (↓∃L:T List. (b L ∈ bag(T)))


Proof




Definitions occuring in Statement :  bag: bag(T) list: List uall: [x:A]. B[x] exists: x:A. B[x] squash: T universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T bag: bag(T) so_lambda: λ2x.t[x] subtype_rel: A ⊆B uimplies: supposing a so_apply: x[s] exists: x:A. B[x] prop: quotient: x,y:A//B[x; y] and: P ∧ Q all: x:A. B[x] implies:  Q squash: T
Lemmas referenced :  squash_wf exists_wf list_wf equal_wf bag_wf list-subtype-bag permutation_wf equal-wf-base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution pointwiseFunctionalityForEquality extract_by_obid isectElimination thin cumulativity hypothesisEquality hypothesis sqequalRule lambdaEquality applyEquality because_Cache independent_isectElimination pertypeElimination productElimination equalityTransitivity equalitySymmetry lambdaFormation rename dependent_pairFormation imageMemberEquality baseClosed dependent_functionElimination independent_functionElimination productEquality imageElimination isect_memberEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[b:bag(T)].    (\mdownarrow{}\mexists{}L:T  List.  (b  =  L))



Date html generated: 2017_10_01-AM-08_44_54
Last ObjectModification: 2017_07_26-PM-04_30_25

Theory : bags


Home Index