proposition: Fact push_exactly_length l : length (push_exactly l) = length l.
proof: Proof. unfold push_exactly. now rewrite half_tile_length, rev_length. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(tiles_solvable bsm_defs)