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


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
  ============================
  (forall x : A, B x) <-> (forall x : A, C x)
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  ============================
  (forall x : A, B x) -> forall x : A, C x
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  H0 : forall x : A, B x
  ============================
  forall x : A, C x
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  H0 : forall x : A, B x
  x : A
  ============================
  C x
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  H0 : forall x : A, B x
  x : A
  H1 : B x <-> C x
  ============================
  C x
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  H0 : forall x : A, B x
  x : A
  H1 : B x -> C x
  H2 : C x -> B x
  ============================
  C x
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  H0 : forall x : A, B x
  x : A
  H1 : B x -> C x
  H2 : C x -> B x
  ============================
  C x
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  H0 : forall x : A, B x
  x : A
  H1 : B x -> C x
  H2 : C x -> B x
  ============================
  C x
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  H0 : forall x : A, B x
  x : A
  H1 : B x -> C x
  H2 : C x -> B x
  H3 : B x
  ============================
  C x
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  H0 : forall x : A, B x
  x : A
  H2 : C x -> B x
  H3 : B x
  H1 : C x
  ============================
  C x
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  ============================
  (forall x : A, C x) -> forall x : A, B x
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  H0 : forall x : A, C x
  ============================
  forall x : A, B x
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  H0 : forall x : A, C x
  x : A
  ============================
  B x
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  H0 : forall x : A, C x
  x : A
  H1 : B x <-> C x
  ============================
  B x
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  H0 : forall x : A, C x
  x : A
  H1 : B x -> C x
  H2 : C x -> B x
  ============================
  B x
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  H0 : forall x : A, C x
  x : A
  H1 : B x -> C x
  H2 : C x -> B x
  ============================
  B x
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  H0 : forall x : A, C x
  x : A
  H1 : B x -> C x
  H2 : C x -> B x
  ============================
  B x
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  H0 : forall x : A, C x
  x : A
  H1 : B x -> C x
  H2 : C x -> B x
  H3 : C x
  ============================
  B x
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  H0 : forall x : A, C x
  x : A
  H1 : B x -> C x
  H2 : C x -> B x
  H3 : C x
  ============================
  B x
Debug:
  
  A : Type
  B, C : A -> Prop
  H : forall x : A, B x <-> C x
  H0 : forall x : A, C x
  x : A
  H1 : B x -> C x
  H3 : C x
  H2 : B x
  ============================
  B x