Using the transitivity of equivalence to rewrite a goal

Question

I want to prove the following theorem:

Theorem T5:
  forall s t, (forall u, OoS s u <-> OoS t u) -> s = t.

My current context and goal are:

1 subgoal
s, t : Entity
H : forall u : Entity, OoS s u <-> OoS t u
______________________________________(1/1)
(forall v : Entity, OoS s v <-> OoS s v \/ OoS t v) /\
(forall v : Entity, OoS t v <-> OoS s v \/ OoS t v)

I was wondering if it’s possible to use the equivalence of the implication to rewrite the goal as forall v : Entity, OoS s v <-> OoS t v as the right part of both equivalence are the same. And then I would use the assumption tactic to finish my proof. But I don’t know if it’s possible to do so and how to do it.

Answer 1

You can rewrite with any equivalence relation in an adequately congruent context using setoid rewriting, see this documentation page.

In your specific case, here is how it would look like:

From Coq Require Import Setoid.

Context (Entity : Type) (OoS : Entity -> Entity -> Prop)
        (s t : Entity) (H : forall v, OoS s v <-> OoS t v).
    enter code here

Goal (forall v : Entity, OoS s v <-> OoS s v \/ OoS t v) /\
       (forall v : Entity, OoS t v <-> OoS s v \/ OoS t v).
Proof.
  split; intros v; rewrite H; intuition.
Qed.

I split the conjunction and introduce v so that rewrite H properly unify OoS s ?x (there might be a way to do without using setoid rewriting under a binder but I am not really fluent with these techniques).