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