proposition: Lemma op_compatible_cons {σ : 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: Proof. intros a b R. exact (P (x,a) (x,b) (EquivRel_Reflexive x, R)). Defined.
imports: HoTT.HProp HoTT.Classes.interfaces.canonical_names HoTT.Classes.interfaces.ua_algebra