proposition: Fact mma_transfert_length : length mma_transfert = 3.
proof: Proof. reflexivity. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool gcd pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs)