proposition: Lemma rev_dec_unique : In (mm2_dec_a 1) M -> In (mm2_dec_b 1) M -> False.
proof: Proof. Proof using HM. move=> /(@In_nth_error mm2_instr) [p /nth_error_Some_mm2_instr_at_iff Hp]. move=> /(@In_nth_error mm2_instr) [q /nth_error_Some_mm2_instr_at_iff Hq]. suff: (S p, (1, 0)) = (S q, (0, 1)) by case. apply: (HM); eexists; by split; [eassumption|constructor]. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun