fact: Definition not_contrapositive `(f : B -> A) : not A -> not B := functor_arrow f idmap.
imports: Basics.Overture Basics.PathGroupoids Basics.Decidable Basics.Equivalences Basics.Trunc Basics.Tactics Types.Forall