fact: Definition flip `{P : A -> B -> Type} : (forall a b, P a b) -> (forall b a, P a b) := fun f b a => f a b.
imports: Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics Basics.Trunc Basics.Contractible Basics.Trunc (istrunc_forall)