---

Step * of Lemma hw5_3_1

T:Type. C:. P:T  .  ((x:T. (C  (P x)))  C  (x:T. (P x)))
BY
{ ((Auto THEN D 4) THEN D 5 THEN Auto THEN InstConcl [x] THEN Auto) }


\mforall{}T:Type.  \mforall{}C:\mBbbP{}.  \mforall{}P:T  {}\mrightarrow{}  \mBbbP{}.    ((\mexists{}x:T.  (C  {}\mRightarrow{}  (P  x)))  {}\mRightarrow{}  C  {}\mRightarrow{}  (\mexists{}x:T.  (P  x)))


By

((Auto  THEN  D  4)  THEN  D  5  THEN  Auto  THEN  InstConcl  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)



Home Index