Definition issymmetric_symmetric_closure {V : UU} (E : V → V → UU) : issymmetric (symmetric_closure E) := λ u v, weqcoprodcomm (E u v) (E v u).
Require Import UniMath.Combinatorics.Lists. Require Import UniMath.MoreFoundations.Subtypes.