Function prop::and::from_imply

pub fn from_imply<A: DProp, B: Prop>(f: Not<Imply<A, B>>) -> And<A, Not<B>>

¬(a => b) => (a ∧ ¬b).