{σ : Signature} {A : Algebra σ} (Φ : ∀ s, Relation (A s)) `{!IsCongruence A Φ} (s : Sort σ) (w : SymbolType σ) (f : Operation A (s ::: w)) (x : A s) (P : OpCompatible A Φ f) : OpCompatible A Φ (f x). Proof. intros a b R. exact (P (x,a) (x,b) (EquivRel_Reflexive x, R)). Defined.
Require Import Import algebra_notations ne_list.notations.