Nuprl Lemma : eo-record-type_wf
∀r:eo_record{i:l}(). (eo-record-type{i:l}(r) ∈ Atom ─→ 𝕌')
Proof
Definitions occuring in Statement : 
eo-record-type: eo-record-type{i:l}(r)
, 
eo_record: eo_record{i:l}()
, 
all: ∀x:A. B[x]
, 
member: t ∈ T
, 
function: x:A ─→ B[x]
, 
atom: Atom
, 
universe: Type
Lemmas : 
subtype_rel_self, 
bool_wf, 
Id_wf, 
nat_wf, 
eq_atom_wf, 
eqtt_to_assert, 
assert_of_eq_atom, 
eqff_to_assert, 
equal_wf, 
bool_cases_sqequal, 
subtype_base_sq, 
bool_subtype_base, 
assert-bnot, 
neg_assert_of_eq_atom, 
top_wf, 
eo_record_wf
\mforall{}r:eo\_record\{i:l\}().  (eo-record-type\{i:l\}(r)  \mmember{}  Atom  {}\mrightarrow{}  \mBbbU{}')
Date html generated:
2015_07_17-AM-08_33_43
Last ObjectModification:
2015_01_27-PM-03_00_03
Home
Index