proposition: Lemma lookup_map_seq_is_Some start xs i x : is_Some (map_seq (M:=M A) start xs !! i) ↔ start ≤ i < start + length xs.
proof: Proof. rewrite <-not_eq_None_Some, lookup_map_seq_None. lia. Qed.
imports: Coq(Permutation) stdpp(options)