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:
<coq-core.plugins.ltac::econstructor@0>

Goals:
  
  A : Type
  P : A -> A -> Type
  Q : A -> A -> Type
  X : Reflexive P
  X0 : Reflexive Q
  x : A
  ============================
   (P x x)

  
  A : Type
  P : A -> A -> Type
  Q : A -> A -> Type
  X : Reflexive P
  X0 : Reflexive Q
  x : A
  ============================
   (Q x x)


DEBUG:Going to execute:
reflexivity

Goals:
  
  A : Type
  P : A -> A -> Type
  Q : A -> A -> Type
  X : Reflexive P
  X0 : Reflexive Q
  x : A
  ============================
   (P x x)

  
  A : Type
  P : A -> A -> Type
  Q : A -> A -> Type
  X : Reflexive P
  X0 : Reflexive Q
  x : A
  ============================
   (Q x x)


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::reflexivity@0>

COQC theories/MCOption.v