proposition: Lemma repeat_app_appP {X: Type} {x: X} {xs: list X} {n m: nat} : repeat x n ++ (repeat x m ++ xs) = repeat x (n+m) ++ xs.
proof: Proof. by rewrite repeat_app app_assoc. Qed.
imports: PeanoNat List Lia Undecidability.StackMachines.Util.Nat_facts ssreflect ssrbool ssrfun