title: Can I introduce sound constructor equivalence?
body: <p>Say I've got an <code>Inductive</code> type like</p>
  
  <pre><code>Inductive foo :=
    | a : foo
    | b : foo
    | c : foo.
  </code></pre>
  
  <p>but what I really want is to "identify" <code>b</code> with <code>c</code> - that is, I want to be able to treat them as two different ways of writing the same thing - and be able to rewrite one into the other.</p>
  
  <p>I could introduce it as an axiom:</p>
  
  <pre><code>Axiom b_equiv_c : forall P : foo -&gt; Prop, P b &lt;-&gt; P c.
  </code></pre>
  
  <p>But that's pretty clearly unsound:</p>
  
  <pre><code>Theorem whoops : False.
  Proof.
    assert (b &lt;&gt; c) as H. { discriminate. }
    apply (b_equiv_c (fun x =&gt; x &lt;&gt; c)) in H.
    contradiction H.
    reflexivity.
    Qed.
  </code></pre>
  
  <p>Is there another way to do this, or something like it? I suspect the answer is no, because it would contradict <code>Inductive</code> constructors being injective.</p>
  
  <h3>Current workaround</h3>
  
  <p>I have a relation</p>
  
  <pre><code>Inductive equiv_foo : foo -&gt; foo -&gt; Prop :=
    | equiv_foo_refl (f : foo) : equiv_foo f f
    | equiv_foo_sym (f f' : foo) : equiv_foo f f' -&gt; equiv_foo f' f
    | equiv_foo_b_c : equiv_foo b c.
  </code></pre>
  
  <p>which then lets me define whether or not a proposition is well-defined with respect to it.</p>
  
  <pre><code>Definition wd_wrt_equiv_foo (P : foo -&gt; Prop) : Prop :=
    forall f f' : foo, equiv_foo f f' -&gt; (P f &lt;-&gt; P f').
  </code></pre>
  
  <p>But this is unpleasant. It means that, for my own inductively-defined propositions, I need to add an additional constructor taking an <code>equiv_foo</code> to be able to prove the well-definedness property. (I suspect that just asserting the above property for some proposition would be unsound.)</p>
  
  <p>Can I not tell Coq "this thing, and anything constructed using it, may not be injective"?</p>