proposition: Lemma eclosed_app xs s t : eclosed (closure xs (app s t)) -> eclosed (closure xs s) /\ eclosed (closure xs t).
proof: Proof. move=> /= [/boundE]. tauto. Qed.
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun