Nuprl Lemma : rec-bind-df-init_wf
[A:Type]. [Sx,Sy:A 
Type]. [ix:a:A (Sx a)]. [iy:a:A (Sy a)].
(rec-bind-df-init(ix;iy) 
a:A (Sx a? 
(Sy a? bag(Void)?)))
Proof not projected
Definitions occuring in Statement :
rec-bind-df-init: rec-bind-df-init(ix;iy),
uall: [x:A]. B[x],
unit: Unit,
member: t T,
apply: f a,
function: x:A B[x],
product: x:A B[x],
union: left + right,
void: Void,
universe: Type,
bag: bag(T)
Definitions :
uall: [x:A]. B[x],
member: t T,
rec-bind-df-init: rec-bind-df-init(ix;iy)
Lemmas :
unit_wf2,
empty-bag_wf
\mforall{}[A:Type]. \mforall{}[Sx,Sy:A {}\mrightarrow{} Type]. \mforall{}[ix:a:A {}\mrightarrow{} (Sx a)]. \mforall{}[iy:a:A {}\mrightarrow{} (Sy a)].
(rec-bind-df-init(ix;iy) \mmember{} a:A {}\mrightarrow{} (Sx a? \mtimes{} (Sy a? \mtimes{} bag(Void)?)))
Date html generated:
2012_02_20-PM-02_42_57
Last ObjectModification:
2012_02_13-PM-10_22_25
Home
Index