Nuprl Lemma : F_wf
[C,B,A:
']. (F() 
bag(A 
B C) 
bag(A C) bag(A C))
Proof not projected
Definitions occuring in Statement :
F: F(),
uall: [x:A]. B[x],
member: t T,
function: x:A B[x],
product: x:A B[x],
universe: Type,
bag: bag(T)
Lemmas :
vote2prop_wf,
bag-map_wf,
bag-append_wf,
bag_wf,
member_wf,
permutation_wf,
subtype_rel_wf,
append_wf
\mforall{}[C,B,A:\mBbbU{}']. (F() \mmember{} bag(A \mtimes{} B \mtimes{} C) {}\mrightarrow{} bag(A \mtimes{} C) {}\mrightarrow{} bag(A \mtimes{} C))
Date html generated:
2011_10_21-AM-08_28_07
Last ObjectModification:
2011_07_20-AM-08_57_02
Home
Index