Nuprl Lemma : vote2prop_wf
[C,B,A:
']. (vote2prop() 
C 
B A 
(C A))
Proof not projected
Definitions occuring in Statement :
vote2prop: vote2prop(),
uall: [x:A]. B[x],
member: t T,
function: x:A B[x],
product: x:A B[x],
universe: Type
\mforall{}[C,B,A:\mBbbU{}']. (vote2prop() \mmember{} C \mtimes{} B \mtimes{} A {}\mrightarrow{} (C \mtimes{} A))
Date html generated:
2011_10_21-AM-08_27_43
Last ObjectModification:
2011_07_20-AM-04_44_40
Home
Index