title: How does the "intro ->" in Coq work on context?
body: <p>I am interested in how does dependent-typed theorem provers do substitution on the context. I find a thing called &quot;intro -&gt;&quot; in Coq, as described in:</p>
  <p><a href="https://coq.inria.fr/refman/proof-engine/tactics.html#intropattern-rarrow-ex" rel="nofollow noreferrer">https://coq.inria.fr/refman/proof-engine/tactics.html#intropattern-rarrow-ex</a></p>
  <p>In the example, it says the goal:</p>
  <blockquote>
  <p>x, y, z : nat</p>
  </blockquote>
  <blockquote>
  </blockquote>
  <h2>H : x = y</h2>
  <blockquote>
  <p>y = z -&gt; x = z</p>
  </blockquote>
  <p>will become</p>
  <blockquote>
  <p>x, z : nat</p>
  </blockquote>
  <blockquote>
  <p>H : x = z</p>
  </blockquote>
  <hr />
  <blockquote>
  <p>x = z</p>
  </blockquote>
  <p>after an application of &quot;intros -&gt;&quot;.</p>
  <p>I am not sure how is the step of substituting H:x = y into H:x = z be done, what is the rule of the logic of Coq is this step according to? It seems like a step of rewriting, and according to my current knowledge most of these rewriting are according to equalities, so the replacement from H:x = y into H:x = z should come from an equality like (H:x = y) = (H:x= z) ($\diamond$), but such an equality is ill-formed because, in principle, we require the LHS and RHS of an equality to have the same type, so the well-formedness of such equality ($\diamond$) depends on the assumption that y = z.</p>
  <p>Could someone please help explaining how does &quot;intro -&gt;&quot; work here? Do we need to get &quot;equalities&quot; like ($\diamond$) involved?</p>