Nuprl Lemma : Comm-output_wf
Comm-output() ∈ Type
Proof
Definitions occuring in Statement :
Comm-output: Comm-output(),
member: t ∈ T,
universe: Type
Lemmas :
Comm-state_wf,
ldag_wf,
Id_wf,
tag-by_wf,
PiDataVal_wf
Latex:
Comm-output() \mmember{} Type
Date html generated:
2015_07_23-AM-11_58_13
Last ObjectModification:
2015_01_29-AM-07_40_10
Home
Index