Check prod: Prop -> Prop -> Prop.
(* (fun A B : Prop => (A * B)%type):Prop -> Prop -> Prop
     : Prop -> Prop -> Prop *)