Nuprl Lemma : eo_record_wf
eo_record{i:l}() ∈ 𝕌'
Proof
Definitions occuring in Statement :
eo_record: eo_record{i:l}(),
member: t ∈ T,
universe: Type
Lemmas :
record_wf,
top_wf,
record+_wf,
subtype_rel_self,
bool_wf,
Id_wf,
nat_wf
eo\_record\{i:l\}() \mmember{} \mBbbU{}'
Date html generated:
2015_07_17-AM-08_33_41
Last ObjectModification:
2015_01_27-PM-02_59_59
Home
Index