proposition: Lemma map_composition : forall A B C (f : B -> C) (g : A -> B) (m : [A]), map A C (fun y => f (g y)) m = map B C f (map A B g m).
proof: Proof. intros A B C f g m. refine (match m with inhabits x => _ end). reflexivity. Qed.