proposition: Fact increment_spec i v l m : list_bool_succ l m -> v#>x = l -> (i,increment i) // (i,v) ->> (15+i,v[m/x]).
proof: Proof. Proof using Hxy. revert l m; intros ? ? [ k l | k ] H. apply increment_spec_1; auto. apply increment_spec_2; 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)