Goal:
    A : Type  B : A -> Prop  C : A -> Prop  H : forall x : A, B x <-> C x
  ============================
   ((exists y, B y) <-> (exists y, C y))


DEBUG:Going to execute:
<coq-core.plugins.firstorder::firstorder@0> $1 $2

Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  ============================
  (exists y, B y) <-> (exists y, C y)
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  ============================
  (exists y, B y) -> exists y, C y
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  H0 : exists y, B y
  ============================
  exists y, C y
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  x : A
  H0 : B x
  ============================
  exists y, C y
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  x : A
  H0 : B x
  H1 : B x <-> C x
  ============================
  exists y, C y
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  x : A
  H0 : B x
  H1 : B x -> C x
  H2 : C x -> B x
  ============================
  exists y, C y
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  x : A
  H0 : B x
  H1 : B x -> C x
  H2 : C x -> B x
  ============================
  exists y, C y
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  x : A
  H0 : B x
  H2 : C x -> B x
  H1 : C x
  ============================
  exists y, C y
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  x : A
  H0 : B x
  H1 : C x
  H2 : B x
  ============================
  exists y, C y
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  x : A
  H0 : B x
  H1 : C x
  H2 : B x
  ============================
  C x
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  ============================
  (exists y, C y) -> exists y, B y
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  H0 : exists y, C y
  ============================
  exists y, B y
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  x : A
  H0 : C x
  ============================
  exists y, B y
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  x : A
  H0 : C x
  H1 : B x <-> C x
  ============================
  exists y, B y
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  x : A
  H0 : C x
  H1 : B x -> C x
  H2 : C x -> B x
  ============================
  exists y, B y
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  x : A
  H0 : C x
  H1 : B x -> C x
  H2 : B x
  ============================
  exists y, B y
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  x : A
  H0 : C x
  H2 : B x
  H1 : C x
  ============================
  exists y, B y
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  x : A
  H0 : C x
  H2 : B x
  H1 : C x
  ============================
  B x