bblum

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) => Cend;term implOr : (A | C) & (B => C) => (A => B) => C =  fn (x,g) f => (case x of inl a => g (f a) | inl c => c)