{A B : Type} (u v: A * B) (p : fst u = fst v) (q : snd u = snd v) : path_prod v u p^ q^ = (path_prod u v p q)^. Proof. destruct u, v; simpl in *; destruct p, q. reflexivity. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Require Import Types.Empty.