transport_paths_FlFr' {A B : Type} {f g : A -> B} {x1 x2 : A} (p : x1 = x2) (q : f x1 = g x1) (r : (f x2) = (g x2)) (h : (ap f p) @ r = q @ (ap g p)) : transport (fun x => f x = g x) p q = r. Proof. refine (transport_paths_FlFr _ _ @ _). refine (concat_pp_p _ _ _ @ _). apply moveR_Vp. exact h^. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics.