proposition: Lemma transport : LU2SemiU (s', t0', t1').
proof: Proof. Proof using φ ψ0 ψ1 Hψ0 Hψ1. exists φ', ψ0', ψ1'. constructor. - rewrite /s' /t0' /=. congr arr; rewrite ?substitute_φ'P substitute_ψ0'P ?/φ' ?enumP; by congruence. - rewrite /s' /t1' /=. congr arr; rewrite ?substitute_φ'P substitute_ψ1'P ?/φ' ?enumP; by congruence. Qed.
imports: List Undecidability.SemiUnification.SemiU Undecidability.SemiUnification.Util(Enumerable) ssreflect ssrfun ssrbool