{A B} (f : A -> B) {x y : A} (p : x = y) : ap_pp f p^ p @ ((ap_V f p @@ 1) @ concat_Vp (ap f p)) = ap (ap f) (concat_Vp p). Proof. destruct p; reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics.