proposition: Lemma isinj_var_term_algebra {σ} (C : Carriers σ) (s : Sort σ) (x y : C s) : var_term_algebra C s x = var_term_algebra C s y -> x = y.
proof: Proof. intro p. apply reflexive_extend_path_term_algebra_path in p. destruct p as [p1 p2]. by destruct (hset_path2 p1 idpath)^. Qed.
imports: HoTT.Algebra.Universal.Algebra HoTT.HSet HoTT.Classes.interfaces.canonical_names HoTT.Algebra.Universal.Homomorphism HoTT.Algebra.Universal.Congruence