proposition: Lemma transport {p: list constraint} : SSemiU p -> RU2SemiU (σ false p, σ true p, τ p).
proof: Proof. move=> [φ'] [ψ0'] [ψ1'] /Forall_forall Hp. exists (φ φ'), (ψ φ' ψ0'), (ψ φ' ψ1'). suff: forall i, substitute (ψ φ' (if i then ψ1' else ψ0')) (substitute (φ φ') (σ i p)) = substitute (φ φ') (τ p) by (move=> H; rewrite (H false) (H true)). move=> i. elim: p Hp. - by move: i => [|] _ /=; rewrite /φ ?enumP /= /ψ ?enumP /=. - move=> [[a x] [y b]] p IH /Forall_cons_iff /=. move => [+ /IH <-]. move Hφ'y: (φ' y) => φ'y. case: φ'y Hφ'y; first done. move=> s t Hφ'y Hst {IH}. move: i a b Hst Hφ'y => [|] [|] [|] -> Hφ'y; by rewrite /= /φ ?enumP /= /ψ ?enumP /= Hφ'y ?substitute_ψP. Qed.
imports: List Undecidability.SemiUnification.SemiU Undecidability.SemiUnification.Util(Enumerable) ssreflect ssrfun ssrbool