Nuprl Lemma : locknd-deq_wf
locknd-deq() ∈ EqDecider(LocKnd)
Proof
Definitions occuring in Statement :
locknd-deq: locknd-deq(),
LocKnd: LocKnd,
deq: EqDecider(T),
member: t ∈ T
Lemmas :
product-deq_wf,
Id_wf,
Knd_wf,
id-deq_wf,
Kind-deq_wf,
subtype_rel-deq,
assert_wf,
hasloc_wf,
member_wf,
equal_wf,
set_wf
locknd-deq() \mmember{} EqDecider(LocKnd)
Date html generated:
2015_07_17-AM-09_14_19
Last ObjectModification:
2015_01_28-AM-07_54_59
Home
Index