proposition: Lemma repeat_app' {X: Type} {x: X} {n m: nat} : repeat x n ++ repeat x m = repeat x (n + m).
proof: Proof. by apply /esym /repeat_app. Qed.
imports: PeanoNat List Lia Undecidability.StackMachines.Util.Nat_facts ssreflect ssrbool ssrfun