fact: Definition unit_setoid@{t u} : Setoid@{t u} poly_unit@{t} := {| equiv := @eq poly_unit@{t} ; setoid_equiv := @eq_equivalence@{t u} poly_unit@{t} |}.
imports: Coq.Classes.RelationClasses Coq.Setoids.Setoid Coq.Vectors.Fin Category.Lib.Foundation