Nuprl Lemma : bag-valueall-type

[T:Type]. valueall-type(bag(T)) supposing valueall-type(T)


Proof




Definitions occuring in Statement :  bag: bag(T) valueall-type: valueall-type(T) uimplies: supposing a uall: [x:A]. B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a bag: bag(T) so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] valueall-type: valueall-type(T) has-value: (a)↓ prop:
Lemmas referenced :  quotient-valueall-type list_wf permutation_wf permutation-equiv list-valueall-type equal-wf-base bag_wf base_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 lambdaEquality independent_isectElimination because_Cache isect_memberEquality axiomSqleEquality equalityTransitivity equalitySymmetry universeEquality

Latex:
\mforall{}[T:Type].  valueall-type(bag(T))  supposing  valueall-type(T)



Date html generated: 2016_05_15-PM-02_21_26
Last ObjectModification: 2015_12_27-AM-09_55_30

Theory : bags


Home Index