Nuprl Lemma : bm_compare_wf
∀[K:Type]. (bm_compare(K) ∈ Type)
Proof
Definitions occuring in Statement :
bm_compare: bm_compare(K),
uall: ∀[x:A]. B[x],
member: t ∈ T,
universe: Type
Lemmas :
trans_wf,
le_wf,
anti_sym_wf,
connex_wf,
refl_wf,
equal-wf-T-base,
sym_wf
\mforall{}[K:Type]. (bm\_compare(K) \mmember{} Type)
Date html generated:
2015_07_17-AM-08_19_22
Last ObjectModification:
2015_01_27-PM-00_36_53
Home
Index