proposition: Lemma mm2_mmi_lookup {P: list mm2_instr} {i: nat} : i < length P -> exists (mmi : mm2_instr), P = firstn i P ++ mmi :: skipn (1+i) P.
proof: Proof. elim: i P. { move=> [|mmi' P'] /=; first by lia. move=> _. by eexists. } move=> i IH [|mmi' P'] /=; first by lia. move=> /(iffRL (Nat.succ_lt_mono _ _)) /IH => - [? ?]. eexists. congr cons. by eassumption. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Wellfounded.Transitive_Closure Undecidability.MinskyMachines.MM2 ssreflect ssrbool ssrfun