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