{σ} {A B : Algebra σ} (f g : Homomorphism A B) (p : def_hom f = def_hom g) (q : p#(is_homomorphism_hom f) = is_homomorphism_hom g) : f = g. Proof. destruct f, g. simpl in *. by path_induction. Defined.
Require Import Import algebra_notations ne_list.notations.