proposition: Corollary prod_map_comp_x {E A B C} (f : B -> C) (g : A -> B) (x : E * A) : prod_map f (prod_map g x) = prod_map (fun x => f (g x)) x.
proof: Proof. destruct x; auto. Qed.
imports: Hask.Ltac Coq.Lists.List FunctionalExtensionality