% Convention: Hi are hypotheses, Ci are conclusions.
% Everything after a % is a comment.
% You are not required to comment your tutch proofs.

% Annotated version of proof in Tutch manual.
proof ExNotImpNotAll : (?x:t. ~A(x)) => ~!x:t. A(x) =
begin
  [ ?x:t. ~A(x);                            % H1
    [ !x:t. A(x);                           % H2
      [ c: t, ~A(c);                        % H3
	  A(c);                             % C1:  !E on H2 and c (H3)
	  F ];                              % C2: =>E on H3 and C1
      F ];                                  % C3:  ?E on H1 and H3..C2
    ~!x:t. A(x) ];                          % C4:  ~I on H2..C3
 (?x:t. ~A(x)) => ~!x:t. A(x);              % C5: =>I on H1..C4
end;

proof swap : (?y:t.!x:t.A(x,y)) => (!x:t.?y:t.A(x,y)) =
begin
  [ ?y:t.!x:t.A(x,y);                       % H1
    [ c : t, !x : t.A(x, c);                % H2
      [ d : t;                              % H3
	A(d, c);                            % C1:  !E on H2 and d (H3)
	?y:t.A(d, y) ];                     % C2:  ?I on C1 and c
      !x:t.?y:t.A(x,y) ];                   % C3:  !I on C2 and d
    !x:t.?y:t.A(x,y) ];                     % C4:  ?E on H1 and H2..C3
  (?y:t.!x:t.A(x,y)) => (!x:t.?y:t.A(x,y)); % C5: =>I on H1..C4
end;