Nuprl Lemma : hdataflow-value-type
∀[A,B:Type]. value-type(hdataflow(A;B)) supposing ↓A
Proof
Definitions occuring in Statement :
hdataflow: hdataflow(A;B),
value-type: value-type(T),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
squash: ↓T,
universe: Type
Lemmas :
valueall-type-value-type,
hdataflow_wf,
hdataflow-valueall-type,
equal-wf-base,
base_wf,
squash_wf
\mforall{}[A,B:Type]. value-type(hdataflow(A;B)) supposing \mdownarrow{}A
Date html generated:
2015_07_17-AM-08_04_39
Last ObjectModification:
2015_01_27-PM-00_16_43
Home
Index