fact: Definition PathOverConstant_id {X:Type} {x x':X} (p:x=x') {Z : Type} (z : Z) (z' : Z) : (z = z') = (PathOver p z z').
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA