title: Why can I use the constructor tactic to prove reflexivity?
body: <p>The constructor tactic allows you to discharge a goal which is an inductive datatype by automatically applying constructors. However, definitional equality is not an inductive product in Coq. Then why does Coq accept this proof?</p>
  <pre><code>Example zeqz : 0 = 0. constructor.
  </code></pre>