proposition: Lemma flatten_eq_var_S {xs s x' x's x} : flatten (closure xs s) = flatten (closure (x' :: x's) (var (S x))) -> if s is var _ then True else flatten (closure xs s) = flatten (closure x's (var x)).
proof: Proof. move=> H. have := @flatten_closure_var_bound (x' :: x's) (S x). rewrite -H [in _ = _]H. move: s {H} => [] /=. - done. - move=> ?? /(_ Logic.I) ?. by rewrite flatten_closure_var_S; [lia|]. - move=> ? /(_ Logic.I) ?. by rewrite flatten_closure_var_S; [lia|]. Qed.
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun