Nuprl Lemma : bm_T-left_wf

[T,Key:Type]. ∀[v:binary_map(T;Key)].  bm_T-left(v) ∈ binary_map(T;Key) supposing ↑bm_T?(v)


Proof




Definitions occuring in Statement :  bm_T-left: bm_T-left(v) bm_T?: bm_T?(v) binary_map: binary_map(T;Key) assert: b uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T universe: Type
Lemmas :  binary_map-ext eq_atom_wf bool_wf eqtt_to_assert assert_of_eq_atom subtype_base_sq atom_subtype_base unit_wf2 unit_subtype_base it_wf eqff_to_assert equal_wf bool_cases_sqequal bool_subtype_base assert-bnot neg_assert_of_eq_atom assert_wf bm_T?_wf binary_map_wf
\mforall{}[T,Key:Type].  \mforall{}[v:binary\_map(T;Key)].    bm\_T-left(v)  \mmember{}  binary\_map(T;Key)  supposing  \muparrow{}bm\_T?(v)



Date html generated: 2015_07_17-AM-08_17_50
Last ObjectModification: 2015_01_27-PM-00_40_10

Home Index