proposition: Lemma join_map_map : forall A B (f : A -> B) (m : [[A]]), join B (map [A] [B] (map A B f) m) = map A B f (join A m).
proof: Proof. intros A B f mm. refine (match mm with inhabits x => _ end). reflexivity. Qed.