Nuprl Lemma : bm_E-wf2
∀[T,Key:Type]. (bm_E() ∈ binary-map(T;Key))
Proof
Definitions occuring in Statement :
binary-map: binary-map(T;Key),
bm_E: bm_E(),
uall: ∀[x:A]. B[x],
member: t ∈ T,
universe: Type
Lemmas :
bm_E_wf,
assert_wf,
bm_cnt_prop_wf
\mforall{}[T,Key:Type]. (bm\_E() \mmember{} binary-map(T;Key))
Date html generated:
2015_07_17-AM-08_18_37
Last ObjectModification:
2015_01_27-PM-00_40_03
Home
Index