fact: Fixpoint op_type_equiv o: Equiv (op_type o) := match o with | ne_list.one _ => _: Equiv (carrier _) | ne_list.cons A g => (e A ==> op_type_equiv g)%signature end.
imports: Coq.Lists.List MathClasses.interfaces.abstract_algebra