proposition: Fact compare_stack_eq_spec v : v#>x = v#>y -> exists w, (i,compare_stacks) // (i,v) ->> (p,w) /\ forall z, z <> x -> z <> y -> v#>z = w#>z.
proof: Proof. Proof using Hxy. intros E. destruct (cs_spec_rec v eq_refl eq_refl) as (w & H1 & H2 & H3). exists w; split; 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)