proposition: Lemma mm2_instr_at_unique {P: list mm2_instr} {i op op'} : mm2_instr_at op i P -> mm2_instr_at op' i P -> op = op'.
proof: Proof. move=> /[dup] /mm2_instr_at_pos ->. move=> /nth_error_Some_mm2_instr_at_iff + /nth_error_Some_mm2_instr_at_iff. by move=> -> []. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Wellfounded.Transitive_Closure Undecidability.MinskyMachines.MM2 ssreflect ssrbool ssrfun