proposition: Lemma in_split_rest {X: Type} {x y: X} {L1 L2: list X} : In y (L1 ++ x :: L2) -> x <> y -> In y (L1 ++ L2).
proof: Proof. rewrite ?in_app_iff /=. by firstorder done. Qed.
imports: PeanoNat List Lia Undecidability.StackMachines.Util.Nat_facts ssreflect ssrbool ssrfun