proposition: Lemma substitute_ψP {φ' ψ': valuation} {t: term} : substitute (ψ φ' ψ') (substitute embed_var t) = substitute embed_var (substitute ψ' t).
proof: Proof. elim: t => [x | *] /=; [by rewrite /ψ ?enumP | by f_equal]. Qed.
imports: List Undecidability.SemiUnification.SemiU Undecidability.SemiUnification.Util(Enumerable) ssreflect ssrfun ssrbool