proposition: Fact push_exactly_spec i l v : (i, push_exactly l) // (i,v) ->> (length (push_exactly l)+i,v[(l++v#>x)/x]).
proof: Proof. unfold push_exactly. rewrite <- (rev_involutive l) at 3. eapply half_tile_spec. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(tiles_solvable bsm_defs)