proposition: Fact increment_length i : length (increment i) = 15.
proof: Proof. unfold increment; rew length; auto. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(tiles_solvable bsm_defs)