proposition: Lemma substitute_embed_var {ξ r} : substitute (fun x => ξ (to_nat (x, 0))) r = substitute ξ (substitute embed_var r).
proof: Proof. elim: r; [done | by move=> /=; congruence]. Qed.
imports: List Undecidability.SemiUnification.SemiU Undecidability.SemiUnification.Util(Enumerable) ssreflect ssrfun ssrbool