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