fact: Definition proj s := @proj1_sig (A s) (P s).
imports: Coq.Classes.RelationClasses MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.interfaces.canonical_names MathClasses.theory.categories MathClasses.interfaces.abstract_algebra