proposition: Lemma cons_repeat_app {X: Type} {x: X} {xs: list X} {m: nat} : x :: (repeat x m ++ xs) = (repeat x (m+1) ++ xs).
proof: Proof. by have ->: m + 1 = S m by lia. Qed.
imports: PeanoNat List Lia Undecidability.StackMachines.Util.Nat_facts ssreflect ssrbool ssrfun