environ   == Note the empty environment.
begin
  1: now
       assume A: (P[] implies Q[]) & (not P[] implies Q[]);
              1: P[] or not P[];                            == Excluded Middle
              2: P[] implies Q[] by A;                      == CE
              3: not P[] implies Q[] by A;                  == CE
              4: (P[] or not P[]) implies Q[] by 1, 2, 3;   == Case Analysis
       thus Q[] by 1, 4;                                    == MP
     end;

( (P[] implies Q[]) & (not P[] implies Q[]) ) implies Q[] by 1     == II