proposition: Lemma isinj_ops_term_algebra `{Funext} {σ} (C : Carriers σ) (u : Symbol σ) (a b : DomOperation (CarriersTermAlgebra C) (σ u)) : ops_term_algebra C u a = ops_term_algebra C u b -> a = b.
proof: Proof. intro p. apply reflexive_extend_path_term_algebra_path in p. destruct p as [p1 p2]. destruct (hset_path2 p1 idpath)^. funext i. apply path_extend_path_term_algebra. apply p2. Qed.
imports: HoTT.Algebra.Universal.Algebra HoTT.HSet HoTT.Classes.interfaces.canonical_names HoTT.Algebra.Universal.Homomorphism HoTT.Algebra.Universal.Congruence