proposition: Lemma inv_instr_at_in_combine {i x}: In (i, x) (combine (seq 1 (length mm)) mm) -> mm2_instr_at x i mm.
proof: Proof. move=> /in_split [l] [r] Hlr. exists (map snd l), (map snd r). move: Hlr. suff: forall mm n, combine (seq n (length mm)) mm = l ++ (i, x) :: r -> mm = map snd l ++ x :: map snd r /\ n + length (map snd l) = i by apply. elim: l. { move=> [|mm2i mm'] n /=; [done|]. move=> [-> ->] <-. split; [|lia]. congr cons. elim: mm' (S i). { done. } by move=> > + ? /= => <-. } move=> [i' mm2i'] l IH [|mm2i mm'] n /=; [done|]. move=> [-> ->] /IH [-> <-]. by split; [|lia]. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun