proposition: Fact mm_no_self_loops_app i P Q : mm_no_self_loops (i,P) -> mm_no_self_loops (length P +i,Q) -> mm_no_self_loops (i,P++Q).
proof: Proof. intros H1 H2 j x H. apply subcode_app_invert_right in H. destruct H as [ H | H ]; revert H. + apply H1. + apply H2. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss) Undecidability.MinskyMachines.MM(mm_defs)