proof implOr : (A | C) & (B => C) => (A => B) => C =
begin
  [(A | C) & (B => C);
    [(A => B);
      A | C; % and-elim 1
      B => C; % and-elim 2
      [A; % or-elim
        B;
        C;
      ];
      [C;
        C;
      ];
      C;
    ];
    (A => B) => C;
  ];
  (A | C) & (B => C) => (A => B) => C
end;

term implOr : (A | C) & (B => C) => (A => B) => C =
  fn (x,g) f => (case x of inl a => g (f a) | inl c => c)