Nuprl Lemma : oob-getleft?_wf

[B,A:Type]. ∀[x:one_or_both(A;B)].  (oob-getleft?(x) ∈ bag(A))


Proof




Definitions occuring in Statement :  oob-getleft?: oob-getleft?(x) one_or_both: one_or_both(A;B) bag: bag(T) uall: [x:A]. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T oob-getleft?: oob-getleft?(x) all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a ifthenelse: if then else fi  prop: bfalse: ff
Lemmas referenced :  oob-hasleft_wf bool_wf eqtt_to_assert single-bag_wf oob-getleft_wf assert_wf uiff_transitivity equal-wf-T-base bnot_wf not_wf eqff_to_assert assert_of_bnot empty-bag_wf equal_wf one_or_both_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality hypothesis lambdaFormation unionElimination equalityElimination because_Cache productElimination independent_isectElimination dependent_functionElimination dependent_set_memberEquality equalityTransitivity equalitySymmetry baseClosed independent_functionElimination axiomEquality isect_memberEquality universeEquality

Latex:
\mforall{}[B,A:Type].  \mforall{}[x:one\_or\_both(A;B)].    (oob-getleft?(x)  \mmember{}  bag(A))



Date html generated: 2018_05_21-PM-08_59_20
Last ObjectModification: 2017_07_26-PM-06_22_44

Theory : general


Home Index