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