Nuprl Lemma : rec-bind-df-statetype_wf
[A:Type]. [Sx,Sy:A 
Type]. (rec-bind-df-statetype(A;Sx;Sy) 
Type)
Proof not projected
Definitions occuring in Statement :
rec-bind-df-statetype: rec-bind-df-statetype(A;Sx;Sy),
uall: [x:A]. B[x],
member: t T,
function: x:A B[x],
universe: Type
Definitions :
uall: [x:A]. B[x],
member: t T,
rec-bind-df-statetype: rec-bind-df-statetype(A;Sx;Sy),
type-monotone: Monotone(T.F[T]),
uimplies: b supposing a,
all: x:A. B[x],
so_lambda: 
x.t[x],
so_apply: x[s]
Lemmas :
unit_wf2,
bag_wf,
subtype_rel_product,
subtype_rel_simple_product,
subtype_rel_sum,
subtype_rel_bag
\mforall{}[A:Type]. \mforall{}[Sx,Sy:A {}\mrightarrow{} Type]. (rec-bind-df-statetype(A;Sx;Sy) \mmember{} Type)
Date html generated:
2012_02_20-PM-02_42_51
Last ObjectModification:
2012_02_13-PM-09_14_56
Home
Index