proposition: Fact bsm_instr_compile_length_eq lnk i ii : length (bsm_instr_compile lnk i ii) = bsm_instr_compile_length ii.
proof: Proof. destruct ii as [ | ? [] ]; simpl; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss compiler_correction) Undecidability.StackMachines.BSM(bsm_defs) Undecidability.MinskyMachines.MM(mm_defs mm_utils)