---

Step * 1 of Lemma not_squash_elim


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



1.  P  :  \mBbbP{}@i'
2.  \mneg{}P@i
\mvdash{}  \mneg{}\mdownarrow{}P


By

(D  0  THEN  Auto)



Home Index