proposition: Lemma in_iP_unique {i j n j' n'} : In (i, (j, n)) iP -> In (i, (j', n')) iP -> j = j' /\ n = n'.
proof: Proof. move=> /nth_error_Some_In_iP + /nth_error_Some_In_iP => -> [-> ->]. by constructor. Qed.
imports: Relation_Operators Operators_Properties Lia PeanoNat List Undecidability.StackMachines.Reductions.CM1_HALT_to_SMNdl_UB.SMX_facts Undecidability.StackMachines.Util(Nat_facts List_facts) ssreflect ssrbool ssrfun