proposition: Lemma lookup_map_seqZ_Some start xs i x : map_seqZ (M:=M A) start xs !! i = Some x ↔ start ≤ i ∧ xs !! Z.to_nat (i - start) = Some x.
proof: Proof. rewrite lookup_map_seqZ. case_guard; naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)