fact: Fixpoint op_closed {o: OpType (sorts sign)}: op_type A o → Prop := match o with | ne_list.one x => P x | ne_list.cons _ _ => λ d, ∀ z, P _ z → op_closed (d z) end.
imports: Coq.Classes.RelationClasses MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.interfaces.canonical_names MathClasses.theory.categories MathClasses.interfaces.abstract_algebra