transport_arrow_toconst' {A : Type} {B : A -> Type} {C : Type} {x1 x2 : A} (p : x1 = x2) (f : B x1 -> C) : transport (fun x => B x -> C) p f = f o transport B p^. Proof. destruct p; auto. Defined.
Require Import Basics.Overture Basics.PathGroupoids Basics.Decidable Require Import Types.Forall.