Nuprl Lemma : bag-drop-head

[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x:T].  (bag-drop(eq;[x bs];x) bs)


Proof




Definitions occuring in Statement :  bag-drop: bag-drop(eq;bs;a) bag: bag(T) cons: [a b] deq: EqDecider(T) uall: [x:A]. B[x] universe: Type sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T bag-drop: bag-drop(eq;bs;a) bag-remove1: bag-remove1(eq;bs;a) bag_remove1_aux: bag_remove1_aux(eq;checked;a;as) all: x:A. B[x] so_lambda: so_lambda(x,y,z.t[x; y; z]) top: Top so_apply: x[s1;s2;s3] append: as bs deq: EqDecider(T) implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a eqof: eqof(d) ifthenelse: if then else fi  bfalse: ff exists: x:A. B[x] prop: or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b false: False not: ¬A
Lemmas referenced :  bag_wf deq_wf list_ind_cons_lemma list_ind_nil_lemma bool_wf eqtt_to_assert safe-assert-deq eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule hypothesis sqequalAxiom hypothesisEquality sqequalHypSubstitution isect_memberEquality isectElimination thin because_Cache extract_by_obid cumulativity universeEquality dependent_functionElimination voidElimination voidEquality applyEquality setElimination rename lambdaFormation unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination independent_isectElimination dependent_pairFormation promote_hyp instantiate independent_functionElimination

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[bs:bag(T)].  \mforall{}[x:T].    (bag-drop(eq;[x  /  bs];x)  \msim{}  bs)



Date html generated: 2018_05_21-PM-09_48_50
Last ObjectModification: 2017_07_26-PM-06_30_46

Theory : bags_2


Home Index