proposition: Lemma map_imap_compose {A1 A2 B} (f1 : K → A1 → option B) (f2 : K → A2 → option A1) (m : M A2) : map_imap f1 (map_imap f2 m) = map_imap (λ k x, f2 k x ≫= f1 k) m.
proof: Proof. apply map_eq. intros i. rewrite !map_lookup_imap. by destruct (m !! i). Qed.
imports: Coq(Permutation) stdpp(options)