proposition: Lemma mm2_step_neq_encodes x y x' y' : mm2_step P x y -> encodes_config x x' -> encodes_config y y' -> x' <> y'.
proof: Proof. move=> +++?. subst y'. move: x' => [p c] [[]] > [/mm2_instr_at_pos + H]; case H => > /=. all: try match goal with |- nat -> _ => move=> ? > end. all: move=> -> [->] [? ->] /= [?] [?]. all: move=> /[dup] /κ_inj1 ? /κ_inj2 ?. all: lia. Qed.
imports: ZArith List PeanoNat Lia Relations.Relation_Operators Relations.Operators_Properties Undecidability.MinskyMachines.MM2 Undecidability.CounterMachines.Util.CM1_facts Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun