proposition: Theorem prod_map_comp {E A B C} (f : B -> C) (g : A -> B) : @prod_map B C E f \o @prod_map A B E g = @prod_map A C E (f \o g).
proof: Proof. extensionality x. destruct x; auto. Qed.
imports: Hask.Ltac Coq.Lists.List FunctionalExtensionality