proposition: Lemma pop_exactly_length l i : length (pop_exactly l i) = 2 * (length l).
proof: Proof. induction l as [ | [] ] in i |- *; cbn; try rewrite IHl; lia. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(tiles_solvable bsm_defs)