title: If two constructor expressions of an inductive type are equal in Coq, can I do rewriting based on their corresponding arguments?
body: <p>I do have a 4-tuple inductive type as follows:</p>
  <pre><code>Inductive my_tuple :=
    | abcd : byte -&gt; nat -&gt; byte -&gt; nat -&gt; my_tuple.
  </code></pre>
  <p>and in my context I do have the following:</p>
  <pre><code>H : abcd b1 n1 b2 n2 = abcd b1' n1' b2' n2'
  </code></pre>
  <p>Given the fact that all constructors for inductive types are injective and disjoint (also discussed <a href="https://stackoverflow.com/questions/32662889/how-do-we-know-all-coq-constructors-are-injective-and-disjoint">here</a>), I'm wondering if I can conclude the corresponding arguments are equal (i.e., <code>b1 = b1'</code>, <code>n1 = n1'</code>, <code>b2 = b2'</code>, and <code>n2 = n2'</code>) and then use them to rewrite other
  equations in my proof. If so, how can I do that? I have already seen these posts (<a href="https://stackoverflow.com/questions/32662889/how-do-we-know-all-coq-constructors-are-injective-and-disjoint">here</a> and <a href="https://stackoverflow.com/questions/37490891/decomposing-equality-of-constructors-coq">there</a>) but still couldn't figure out how to do so.</p>
  <p>Thanks in advance for any comments.</p>