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