proposition: Lemma sig_type_refl `{∀ a, Reflexive (e a)} (o: OpType) a (x: op_type (ne_list.cons a o)) y: Proper (=) x → op_type_equiv o (x y) (x y).
proof: Proof. intro H0. apply H0. reflexivity. Qed.
imports: Coq.Lists.List MathClasses.interfaces.abstract_algebra