Nuprl Lemma : aa_dependent_fan

Nuprl Lemma : aa_dependent_fan_contra

(

f:

. Bij(

;

;f))

(

R:

List

((

l1,l2:

List. ((R (l1 @ l2))

(R l1)))

(

A:f:

(

n:

. ((

(f n))

(n > 0))).

x:

. (

(R mklist(x;fst(A)))))

(

x:

.

l:

List. ((x = ||l||)

(R l)))))

Proof not projected

Error : references
(\mexists{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{} {}\mrightarrow{} \mBbbB{}. Bij(\mBbbN{};\mBbbN{} {}\mrightarrow{} \mBbbB{};f)) {}\mRightarrow{} (\mexists{}R:\mBbbB{} List {}\mrightarrow{} \mBbbP{} ((\mforall{}l1,l2:\mBbbB{} List. ((R (l1 @ l2)) {}\mRightarrow{} (R l1))) \mwedge{} (\mforall{}A:f:\mBbbN{} {}\mrightarrow{} \mBbbB{} \mtimes{} (\mexists{}n:\mBbbN{}. ((\muparrow{}(f n)) \mwedge{} (n > 0))). \mexists{}x:\mBbbN{}. (\mneg{}(R mklist(x;fst(A))))) \mwedge{} (\mforall{}x:\mBbbN{}. \mexists{}l:\mBbbB{} List. ((x = ||l||) \mwedge{} (R l))))) Date html generated: 2013_03_20-AM-11_02_18 Last ObjectModification: 2012_11_27-AM-10_32_10 Home Index