proof foo : A & A => A =
begin
[ A & A;  
  A;
];
A & A => A;
end;

proof topc : (T => C) => C =
begin
[ T => C;
  T;
  C;
];
(T => C) => C;
end;

proof impdef : ~A|B => (A => B) =
begin
[ ~A|B;
  [ ~A;
    [ A;
      F;
      B;
    ];
    A => B;
  ];
  [ B;
    [ A;
      B;
    ];
    A => B;
  ];
  A => B;
];
~A|B => (A => B);
end;