fact: Definition copy_stack := move_rev_stack x z i ++ copy_rev_stack z x y (7+i).
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(tiles_solvable bsm_defs)