proposition: Lemma reflection : RU2SemiU (s0, s1, t).
proof: Proof. Proof using φ' ψ0' ψ1' Hψ0' Hψ1'. exists (fun x => φ' (to_nat (x, 0))), ψ0', ψ1'. move: Hψ0' Hψ1'. rewrite ?(substitute_embed_var (ξ := φ')) /s' /t0' /t1' /=. move=> ? ?. constructor; by congruence. Qed.
imports: List Undecidability.SemiUnification.SemiU Undecidability.SemiUnification.Util(Enumerable) ssreflect ssrfun ssrbool