proposition: Lemma pop_many_length k i : length (pop_many k i) = k.
proof: Proof. induction k in i |- *; cbn; congruence. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(tiles_solvable bsm_defs)