`{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. 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.
Require Import