Goal:
    A : Type  R : relation A  S : relation A
  ============================
   (inclusion R S -> inclusion S R -> relation_equivalence R S)


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

Debug:
  
  A : Type
  R : relation A
  S : relation A
  ============================
  inclusion R S -> inclusion S R -> relation_equivalence R S
Debug:
  
  A : Type
  R : relation A
  S : relation A
  X : inclusion R S
  ============================
  inclusion S R -> relation_equivalence R S
Debug:
  
  A : Type
  R : relation A
  S : relation A
  X : inclusion R S
  X0 : inclusion S R
  ============================
  relation_equivalence R S
Debug:
  
  A : Type
  R : relation A
  S : relation A
  X : inclusion R S
  X0 : inclusion S R
  x : A
  ============================
  forall y : A, R x y <~> S x y
Debug:
  
  A : Type
  R : relation A
  S : relation A
  X : inclusion R S
  X0 : inclusion S R
  x, y : A
  ============================
  R x y <~> S x y
Debug:
  
  A : Type
  R : relation A
  S : relation A
  X : inclusion R S
  X0 : inclusion S R
  x, y : A
  ============================
  R x y -> S x y
Debug:
  
  A : Type
  R : relation A
  S : relation A
  X : inclusion R S
  X0 : inclusion S R
  x, y : A
  X1 : R x y
  ============================
  S x y
Debug:
  
  A : Type
  R : relation A
  S : relation A
  X : inclusion R S
  X0 : inclusion S R
  x, y : A
  X1 : R x y
  X2 : forall y : A, R x y -> S x y
  ============================
  S x y
Debug:
  
  A : Type
  R : relation A
  S : relation A
  X : inclusion R S
  X0 : inclusion S R
  x, y : A
  X1 : R x y
  X2 : forall y : A, R x y -> S x y
  X3 : R x y -> S x y
  ============================
  S x y
Debug:
  
  A : Type
  R : relation A
  S : relation A
  X : inclusion R S
  X0 : inclusion S R
  x, y : A
  X1 : R x y
  X2 : forall y : A, R x y -> S x y
  X3 : S x y
  ============================
  S x y
Debug:
  
  A : Type
  R : relation A
  S : relation A
  X : inclusion R S
  X0 : inclusion S R
  x, y : A
  ============================
  S x y -> R x y
Debug:
  
  A : Type
  R : relation A
  S : relation A
  X : inclusion R S
  X0 : inclusion S R
  x, y : A
  X1 : S x y
  ============================
  R x y
Debug:
  
  A : Type
  R : relation A
  S : relation A
  X : inclusion R S
  X0 : inclusion S R
  x, y : A
  X1 : S x y
  X2 : forall y : A, S x y -> R x y
  ============================
  R x y
Debug:
  
  A : Type
  R : relation A
  S : relation A
  X : inclusion R S
  X0 : inclusion S R
  x, y : A
  X1 : S x y
  X2 : forall y : A, S x y -> R x y
  X3 : S x y -> R x y
  ============================
  R x y
Debug:
  
  A : Type
  R : relation A
  S : relation A
  X : inclusion R S
  X0 : inclusion S R
  x, y : A
  X1 : S x y
  X2 : forall y : A, S x y -> R x y
  X3 : R x y
  ============================
  R x y