---

Step * 1 1 1 of Lemma ross_pnp


1. P:. EquivRel(P;p1,p2.True)
2. P : @i'
3. x : P  (P) //True@i
 x  P //True  P //True
BY
{ ((D (-1) THEN Auto)
   THEN Try (BackThruSomeHyp)
   THEN (D -3 THEN D -2 THEN Auto THEN (((EqCD THENM EqTypeCD) THEN Auto) THEN Try (BackThruSomeHyp)))) }



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


By

((D  (-1)  THEN  Auto)
  THEN  Try  (BackThruSomeHyp)
  THEN  (D  -3
              THEN  D  -2
              THEN  Auto
              THEN  (((EqCD  THENM  EqTypeCD)  THEN  Auto)\mcdot{}  THEN  Try  (BackThruSomeHyp))\mcdot{})\mcdot{})



Home Index