Definition reverse_in_closure {V : UU} {E : V → V → UU} {u v : V} (p : gpaths (symmetric_closure E) u v) : gpaths (symmetric_closure E) v u := reverse (issymmetric_symmetric_closure E) p.
Require Import UniMath.Combinatorics.Lists. Require Import UniMath.MoreFoundations.Subtypes.