Nuprl Lemma : bag-single-no-repeats

[T:Type]. ∀[x:T].  bag-no-repeats(T;{x})


Proof




Definitions occuring in Statement :  bag-no-repeats: bag-no-repeats(T;bs) single-bag: {x} uall: [x:A]. B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T single-bag: {x} bag-no-repeats: bag-no-repeats(T;bs) exists: x:A. B[x] and: P ∧ Q cand: c∧ B subtype_rel: A ⊆B uimplies: supposing a prop: squash: T
Lemmas referenced :  cons_wf nil_wf list-subtype-bag no_repeats_singleton equal_wf bag_wf no_repeats_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut dependent_pairFormation extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality hypothesis because_Cache applyEquality independent_isectElimination lambdaEquality sqequalRule independent_pairFormation productEquality imageMemberEquality baseClosed imageElimination isect_memberEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[x:T].    bag-no-repeats(T;\{x\})



Date html generated: 2017_10_01-AM-08_51_46
Last ObjectModification: 2017_07_26-PM-04_33_32

Theory : bags


Home Index