Anomaly "in Univ.repr: Universe Var(0) undefined." with Derive Signature NoConfusion EqDec for Var.

[SkySkimmer]

Require Equations.Prop.Classes.

Set Universe Polymorphism.

Register Equations.Init.sigma as equations.sigma.type.
Register Equations.Init.sigmaI as equations.sigma.intro.
Register Equations.Init.pr1 as equations.sigma.pr1.
Register Equations.Init.pr2 as equations.sigma.pr2.

Register Init.Logic.eq as equations.equality.type.

Register Classes.EqDec as equations.eqdec.class.
Register Classes.dec_eq as equations.eqdec.dec_eq.

Register Init.Logic.False as equations.bottom.type.

Register Init.Logic.True as equations.top.type.

Register Equations.Prop.Classes.NoConfusionPackage as equations.noconfusion.class.

Inductive Ty@{u} : Type@{u} :=
  | TyUnit : Ty.

Inductive Var@{u} : Ty@{u} -> Type@{u} :=
  | ZV x : Var x.

Derive Signature NoConfusion EqDec for Var.

tested with Coq 8.17 and Equations 1.3+8.17, and Coq master and Equations main