---

Step * of Lemma not_squash_elim

P:. (P  P)
BY
{ Auto }

1
1. P : @i'
2. P@i
 P


\mforall{}P:\mBbbP{}.  (\mneg{}P  \mLeftarrow{}{}\mRightarrow{}  \mneg{}\mdownarrow{}P)


By

Auto



Home Index