proposition: Fact main_loop_length : length main_loop = length_main_loop.
proof: Proof. unfold main_loop, length_main_loop, lFD; rew length; lia. Qed.
imports: List Arith Lia Bool Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.StackMachines.BSM(tiles_solvable bsm_defs)