proposition: Fact mm_transfert_length i : length (mm_transfert i) = 3.
proof: Proof. reflexivity. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss) Undecidability.MinskyMachines.MMenv(env mme_defs)