bblum

 22 annotated proof implOr : (A | C) & (B => C) => (A => B) => C = 23 begin 24   [ q : (A | C) & (B => C); 25     [ f : (A => B); 26       fst q : A | C; 27       snd q : B => C; 28     ]; 29   ]; 30   fn q => fn f => case fst q of inl a => (snd q) (f a) | inr c => c : (A | C) & (B => C) => (A => B) => C 31 end;