% Translating A & B => B & A
%query 1 *
{A:o} {B:o}
comb (impliesI [x:! (A & B)] andI (andER x) (andEL x)) (H A B).

% Translating the result back to a natural deduction
%query 1 *
combdefn
  (MP (MP S (MP (MP S (MP K PAIR)) (MP (MP S (MP K RIGHT)) (MP (MP S K) K))))
     (MP (MP S (MP K LEFT)) (MP (MP S K) K)))
D.

% Translating S
%query 1 *
combdefn S D.

% Translating back the natural deduction for S
%query 1 *
comb (impliesI
      ([p:! A1 => A2 => A3]
          impliesI
             ([q:! A1 => A2]
                 impliesI ([r:! A1] impliesE (impliesE p r) (impliesE q r)))))
H.