proposition: Fact mma_div2_branch_length : length mma_div2_branch = 9.
proof: Proof. unfold mma_div2_branch; rew length; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs mma_utils)