{σ : Signature} (A B : Algebra σ) (p : carriers A = carriers B) (q : transport (λ X, ∀ u, Operation X (σ u)) p (operations A) = operations B) : A = B. Proof. destruct A,B. cbn in *. by path_induction. Defined.
Require Import Import ne_list.notations.