title: Coq: apply the f_equal tactic only when f is an inductive constructor
body: <p>The <code>f_equal</code> tactic is unconditionally useful for equality proofs involving inductive constructors. <code>a :: s = a' :: s</code> would be such a goal, reducing to <code>a = a'</code>.</p>
  
  <p>Using it with arbitrary functions is a different story. <code>4 mod 2 = 2 mod 2</code> would reduce to <code>4 = 2</code>, which is clearly absurd.</p>
  
  <p>I'm wondering if there's a way to automatically apply <code>f_equal</code> (or similar) <strong>only</strong> in cases where it doesn't lose information, e.g. inductive constructors.</p>