{X Y Z : Type} {f g : X -> Y -> Z} (h : forall x y, f x y = g x y) (x : X) (y : Y) : ap100 (equiv_path_arrow2 f g h) x y = h x y. Proof. unfold ap100. refine (ap (fun p => ap10 p y) _ @ _). 1: apply apD10_path_arrow. cbn. apply apD10_path_arrow. Defined.
Require Import Basics.Overture Basics.PathGroupoids Basics.Decidable Require Import Types.Forall.