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