proposition: Lemma ap_pp_concat_Vp {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: Proof. destruct p; reflexivity. Defined.
imports: Basics.Overture Basics.Tactics