{σ} (C : Carriers σ) (s : Sort σ) (x y : C s) : var_term_algebra C s x = var_term_algebra C s y -> x = y. Proof. intro p. apply reflexive_extend_path_term_algebra_path in p. destruct p as [p1 p2]. by destruct (hset_path2 p1 idpath)^. Qed.
Require Import