proposition: Lemma eclosed_closed_flatten x : eclosed x -> closed (flatten x).
proof: Proof. elim /(induction_ltof1 _ eterm_size) : x. move=> [ctx s] /= IH [Hs] Hctx. apply /closed_dcl. apply: bound_subst_many; [|by rewrite map_length]. rewrite map_map. apply /all_Forall /Forall_forall => y Hy. apply: IH. - rewrite /ltof /=. move: Hy => /(@in_split eterm) [?] [?] ->. rewrite map_app /= list_sum_app /= term_size_S. lia. - move: Hctx => /all_Forall /Forall_forall. by apply. Qed.
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun