proposition: Lemma lookup_map_seq start xs i : map_seq (M:=M A) start xs !! i = (guard (start ≤ i);; xs !! (i - start)).
proof: Proof. revert start. induction xs as [|x' xs IH]; intros start; simpl. { rewrite lookup_empty; simplify_option_eq; by rewrite ?lookup_nil. } destruct (decide (start = i)) as [->|?]. - by rewrite lookup_insert, option_guard_True, Nat.sub_diag by lia. - rewrite lookup_insert_ne, IH by done. simplify_option_eq; try done || lia. by replace (i - start) with (S (i - S start)) by lia. Qed.
imports: Coq(Permutation) stdpp(options)