title: How to define an automatically unfoldable definition
body: <p>I sometimes want to define some shortcut for existing functions like in the following example:</p>
  
  <pre><code>Parameter T : Set.
  Parameter zero one: T.
  Parameter f : T -&gt; T -&gt; option T.
  Hypothesis f_unit : forall t, f zero t = None.
  
  Definition g (t : T) := f t one.
  </code></pre>
  
  <p>However, this definition seems to be abstract since I cannot use theorems about <code>f</code> on instances of <code>g</code> without first unfolding:</p>
  
  <pre><code>Goal (g zero = None).
    unfold g.
    rewrite f_unit.
    reflexivity.
  Qed.
  </code></pre>
  
  <p>Is there a way to mark definitions as automatically unfoldable?</p>