proposition: Lemma map_compose_as_fold m n : m ∘ₘ n = map_fold (λ a b, match m !! b with | Some c => <[a:=c]> | None => id end) ∅ n.
proof: Proof. apply (map_fold_ind (λ mn n, omap (m !!.) n = mn)). { apply map_compose_empty_r. } intros k b n' mn Hn' IH. rewrite omap_insert, <-IH. destruct (m !! b); [done|]. by apply delete_notin, map_lookup_compose_None_2_1. Qed.
imports: Coq(Permutation) stdpp(options)