Nuprl Lemma : nat-missing-type_wf
nat-missing-type() ∈ Type
Proof
Definitions occuring in Statement :
nat-missing-type: nat-missing-type(),
member: t ∈ T,
universe: Type
Lemmas :
le_wf,
list_wf,
nat_wf,
l-ordered_wf,
less_than_wf,
l_all_wf2,
l_member_wf
nat-missing-type() \mmember{} Type
Date html generated:
2015_07_17-AM-08_21_22
Last ObjectModification:
2015_04_02-PM-05_43_05
Home
Index