Nuprl Lemma : contrapos

Nuprl Lemma : contrapos_elim

(

P:

. (

P

(

P)))

(

P,Q:

. (

((

Q)

(

P))

(

P)

(

Q)))

Proof not projected

Error : references
(\mforall{}P:\mBbbP{}. (\mdownarrow{}P \mvee{} (\mneg{}P))) {}\mRightarrow{} (\mforall{}P,Q:\mBbbP{}. (\mdownarrow{}((\mneg{}\mdownarrow{}Q) {}\mRightarrow{} (\mneg{}\mdownarrow{}P)) {}\mRightarrow{} (\mdownarrow{}P) {}\mRightarrow{} (\mdownarrow{}Q))) Date html generated: 2013_03_20-AM-11_02_10 Last ObjectModification: 2013_02_25-PM-04_45_25 Home Index