{A B : Type} {x' y' z' : B} (f : A -> (x' = y')) (g : A -> (y' = z')) {x y : A} (p : x = y) : (ap f p) @@ (ap g p) = ap (fun u => f u @ g u) p. Proof. by path_induction. Defined.
Require Import Basics.Overture Basics.Tactics.