title: Coq: Rewriting between two equivalent setoids
body: <p>I have two setoids and bisimilar:</p>
  <p>Definition of <a href="https://github.com/awalterschulze/regex-reexamined-coq/tree/edafc1c98311eeda8ec7d30237b14c2eeddfc1ce/src/Brzozowski/Language.v#L25" rel="nofollow noreferrer">lang_iff</a>:</p>
  <pre><code>Definition lang := str -&gt; Prop.
  Definition lang_iff (s1 s2: lang): Prop :=
    forall (s: str),
    s \in s1 &lt;-&gt; s \in s2.
  </code></pre>
  <p>The setoid <a href="https://github.com/awalterschulze/regex-reexamined-coq/tree/edafc1c98311eeda8ec7d30237b14c2eeddfc1ce/src/Brzozowski/Setoid.v" rel="nofollow noreferrer">lang_setoid</a>:</p>
  <pre><code>Add Parametric Relation: lang lang_iff
    reflexivity proved by lang_iff_refl
    symmetry proved by lang_iff_sym
    transitivity proved by lang_iff_trans as lang_setoid.
  </code></pre>
  <p>Definition of <a href="https://github.com/awalterschulze/regex-reexamined-coq/tree/edafc1c98311eeda8ec7d30237b14c2eeddfc1ce/src/Coinduction/Bisimilar.v#L8" rel="nofollow noreferrer">bisimilar</a>:</p>
  <pre><code>CoInductive bisimilar : lang -&gt; lang -&gt; Prop :=
    | bisim : forall (P Q: lang),
      ...
      -&gt; bisimilar P Q.
  </code></pre>
  <p>The <a href="https://github.com/awalterschulze/regex-reexamined-coq/tree/edafc1c98311eeda8ec7d30237b14c2eeddfc1ce/src/Coinduction/Setoid.v" rel="nofollow noreferrer">bisimilar_setoid</a>:</p>
  <pre><code>Add Parametric Relation: lang bisimilar
    reflexivity proved by bisimilar_refl
    symmetry proved by bisimilar_sym
    transitivity proved by bisimilar_trans as bisimilar_setoid.
  </code></pre>
  <p>These are <a href="https://github.com/awalterschulze/regex-reexamined-coq/tree/edafc1c98311eeda8ec7d30237b14c2eeddfc1ce/src/Coinduction/Bisimilar.v#L82" rel="nofollow noreferrer">proven to be equivalent</a>:</p>
  <pre><code>Theorem bisimilar_is_equivalence:
    forall (P Q: lang),
    bisimilar P Q &lt;-&gt; lang_iff P Q.
  </code></pre>
  <p>I can manually rewrite between them with some acrobatics, but was wondering if there is a way to help Coq to see that it can rewrite between two setoids and make the following possible without <code>Fail</code>:</p>
  <pre><code>Example example_rewriting_using_lang_iff_in_bisimilar:
    forall (P Q: lang)
    (pq: lang_iff P Q),
    bismilar Q P.
  Proof.
  intros.
  Fail rewrite pq.
  Fail reflexivity.
  Abort.
  </code></pre>
  <p>The reason for this question is that it is useful to take some steps with coinduction in bisimilar and then resolve an equivalence with lang_iff.</p>
  <p>A second part of this question is whether we need to preprove all the morphisms from lang_iff in bimisilar or if there is some command to reuse them?</p>