iff_not@{u v k | u <= k, v <= k} (A : Type@{u}) (B : Type@{v}) : A <-> B -> iff@{u v k} (~A) (~B). Proof. intros e; split; apply not_contrapositive@{_ k}, e. Defined.
Require Import Basics.Overture Basics.PathGroupoids Basics.Decidable Require Import Types.Forall.