proposition: Lemma flatten_app xs s t : flatten (closure xs (app s t)) = app (flatten (closure xs s)) (flatten (closure xs t)).
proof: Proof. done. Qed.
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun