Nuprl Lemma : bag-deq_wf

[T:Type]. ∀[eq:EqDecider(T)].  (bag-deq(eq) ∈ EqDecider(bag(T)))


Proof




Definitions occuring in Statement :  bag-deq: bag-deq(eq) bag: bag(T) deq: EqDecider(T) uall: [x:A]. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T bag-deq: bag-deq(eq) deq: EqDecider(T) all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q prop: rev_implies:  Q uiff: uiff(P;Q) uimplies: supposing a so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  bag-eq_wf bag_wf equal_wf assert-bag-eq assert_wf all_wf iff_wf deq_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule dependent_set_memberEquality lambdaEquality lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis lambdaFormation independent_pairFormation because_Cache addLevel allFunctionality productElimination impliesFunctionality independent_isectElimination applyEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].    (bag-deq(eq)  \mmember{}  EqDecider(bag(T)))



Date html generated: 2016_05_15-PM-08_00_43
Last ObjectModification: 2015_12_27-PM-04_15_57

Theory : bags_2


Home Index