Fix (as in make rigid) the universes of the inductive family in NoConfusionHom derivations
Fix (as in make rigid) the universes of the inductive family in
NoConfusionHom derivations

mattam82/Coq-Equations,mattam82/Coq-Equations