pub fn flip_neg_left<A: DProp, B: Prop>(f: Imply<Not<A>, B>) -> Imply<Not<B>, A>
(¬a => b) => (¬b => a).
(¬a => b) => (¬b => a)
