proposition: Lemma length_M' : length M' = a0+b0+length M.
proof: Proof. by rewrite /M' !app_length !repeat_length map_length Nat.add_assoc. Qed.
imports: List PeanoNat Lia Relations.Relation_Operators Relations.Operators_Properties Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun