Proof of Nuprl Lemma : excluded-middle-lower-level

Step * of Lemma excluded-middle-lower-level

(

P:

'. (

P

(

P)))

(

P:

. (

P

(

P)))
BY
{ Auto }

(\mforall{}P:\mBbbP{}'. (\mdownarrow{}P \mvee{} (\mneg{}P))) {}\mRightarrow{} (\mforall{}P:\mBbbP{}. (\mdownarrow{}P \mvee{} (\mneg{}P))) By Auto Home Index