---

Step * 1 of Lemma double_neg_elim


1. P:. (P  (P))@i'
2. P : @i'
3. P
 P
BY
{ (D 0 THEN MaAuto) }



1.  \mforall{}P:\mBbbP{}.  (\mdownarrow{}P  \mvee{}  (\mneg{}P))@i'
2.  P  :  \mBbbP{}@i'
3.  \mneg{}P
\mvdash{}  \mneg{}\mdownarrow{}P


By

(D  0  THEN  MaAuto)



Home Index