horizon := 0;;

thm `;
  assume ?x:A. T [1];
  let P be A->bool;
  thus ?x. P x ==> !y. P y
  proof
    (?x. ~P x) \/ ~(?x. ~P x);  // LEM
    cases by -;                 // \/E
    suppose ?x. ~P x;
      consider x such that
        ~P x [2] by -;          // ?E
      take x;                   // ?I
      assume P x;               // ==>I
      F by 2,-;                 // ~E
    qed by -;                   // FE
    suppose ~(?x. ~P x) [3];
      consider x such that
        (\x:A. T) x by 1;       // ?E
      take x;                   // ?I
      assume P x;               // ==>I
      let y be A;               // !I
      P y \/ ~P y;              // LEM
      cases by -;               // \/E
      suppose P y;
      qed by -;                 //
      suppose ~P y;
        ?y. ~P y
        proof
          take y;               // ?I
        qed by -;               //
        F by 3,-;               // ~E
      qed by -;                 // FE
    end;
  end`;;