fact: 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.
imports: UniMath.Combinatorics.Lists UniMath.MoreFoundations.Subtypes