---

Step * 1 of Lemma ross_pnp


1. P:. EquivRel(P;p1,p2.True)
2. P : @i'
3. P  (P) //True@i
 P //True  P //True
BY
{ RenameVar  `x' (-1) }

1
1. P:. EquivRel(P;p1,p2.True)
2. P : @i'
3. x : P  (P) //True@i
 P //True  P //True



1.  \mforall{}P:\mBbbP{}.  EquivRel(P;p1,p2.True)
2.  P  :  \mBbbP{}@i'
3.  P  \mvee{}  (\mneg{}P)  //True@i
\mvdash{}  P  //True  \mvee{}  \mneg{}P  //True


By

RenameVar    `x'  (-1)



Home Index