Nuprl Lemma : FOStruct_wf
∀[Dom:Type]. (FOStruct(Dom) ∈ 𝕌')
Proof
Definitions occuring in Statement :
FOStruct: FOStruct(Dom),
uall: ∀[x:A]. B[x],
member: t ∈ T,
universe: Type
Lemmas :
list_wf
\mforall{}[Dom:Type]. (FOStruct(Dom) \mmember{} \mBbbU{}')
Date html generated:
2015_07_17-AM-07_53_08
Last ObjectModification:
2015_01_27-AM-10_07_09
Home
Index