proposition: Lemma reflection {p: list constraint} : RU2SemiU (σ false p, σ true p, τ p) -> SSemiU p.
proof: Proof. move=> [φ] [ψ0] [ψ1] [Hψ0 Hψ1]. exists (fun x => φ (to_nat (x, 0))), ψ0, ψ1. rewrite -Forall_forall. elim: p Hψ0 Hψ1; first done. move=> [[a x] [y b]] p IH /= [Hψ0 ?] [Hψ1 ?]. constructor; [| by apply: IH]. by move: a Hψ0 Hψ1 => /= [_ <-| <- _]; move: b => [|]. Qed.
imports: List Undecidability.SemiUnification.SemiU Undecidability.SemiUnification.Util(Enumerable) ssreflect ssrfun ssrbool