---

Step * of Lemma fim97_lift_exist

C:. T:Type. P:T  .  ((R:. (R  (R)))  (C  (t:T. (P t)))  (a:T. (t:T. (C  (P t)))))
BY
{ (Auto THEN InstHyp [t:T. (P t)] 4 THEN Auto THEN D (-1) THEN MaAuto) }


\mforall{}C:\mBbbP{}.  \mforall{}T:Type.  \mforall{}P:T  {}\mrightarrow{}  \mBbbP{}.
    ((\mforall{}R:\mBbbP{}.  (\mdownarrow{}R  \mvee{}  (\mneg{}R)))  {}\mRightarrow{}  (C  {}\mRightarrow{}  (\mdownarrow{}\mexists{}t:T.  (P  t)))  {}\mRightarrow{}  (\mforall{}a:T.  (\mdownarrow{}\mexists{}t:T.  (C  {}\mRightarrow{}  (P  t)))))


By

(Auto  THEN  InstHyp  [\mkleeneopen{}\mdownarrow{}\mexists{}t:T.  (P  t)\mkleeneclose{}]  4\mcdot{}  THEN  Auto  THEN  D  (-1)  THEN  MaAuto)



Home Index