Definition cons {V : UU} {E : V → V → UU} {w u v : V} (e : E u v) (p : gpaths E v w) : gpaths E u w := (S (pr1 p),, (v,, (e,, pr2 p))).
Require Import UniMath.Combinatorics.Lists. Require Import UniMath.MoreFoundations.Subtypes.