proposition: Lemma lookup_map_seq_Some_inv start xs i x : xs !! i = Some x ↔ map_seq (M:=M A) start xs !! (start + i) = Some x.
proof: Proof. rewrite lookup_map_seq, option_guard_True by lia. by rewrite Nat.add_sub_swap, Nat.sub_diag. Qed.
imports: Coq(Permutation) stdpp(options)