Goal:
    A : Type  P : A -> A -> Type  Q : A -> A -> Type
  ============================
   (Reflexive P -> Reflexive Q -> Reflexive (fun x y : A => P x y × Q x y))


DEBUG:Going to execute:
econstructor