title: Coq: Bypassing the uniform inheritance condition
body: <p>I've trouble understanding the (point of the) <a href="https://coq.inria.fr/distrib/current/refman/addendum/implicit-coercions.html?implicit%20coercions#identity-coercions" rel="nofollow noreferrer">gauntlet</a> one has to pass to bypass the uniform inheritance condition (UIC). Per the instruction</p>
  
  <blockquote>
    <p>Let /.../ <code>f: forall (x₁:T₁)..(xₖ:Tₖ)(y:C u₁..uₙ), D v₁..vₘ</code> be a
    function which does not verify the uniform inheritance condition. To
    declare <code>f</code> as coercion, one has first to declare a subclass <code>C'</code> of <code>C</code>
    /.../</p>
  </blockquote>
  
  <p>In the code below, <code>f</code> is such a function:</p>
  
  <pre><code>Parameter C: nat -&gt; Type.
  Parameter D: nat -&gt; Prop.
  Parameter f: forall {x y}(z:C x), D y.
  Parameter f':&gt; forall {x y}(z:C x), D y. (*violates uic*)
  Print Coercions. (* @f' *)
  </code></pre>
  
  <p>Yet I do not have to do anything except putting <code>:&gt;</code> to declare it as a coercion. Maybe the gauntlet will somehow help to avoid breaking UIC? Not so:</p>
  
  <pre><code>Definition C' := fun x =&gt; C x.
  Fail Definition Id_C_f := fun x d (y: C' x) =&gt; (y: C d). (*attempt to define Id_C_f as in the manual*)
  Identity Coercion Id_C_f: C' &gt;-&gt; C.
  Fail Coercion f: C' &gt;-&gt; D. (*Cannot recognize C' as a source class of f*)
  Coercion f'' {x y}(z:C' x): D y := f z. (*violates uic*)
  Print Coercions. (* @f' @f'' Id_C_f *)
  </code></pre>
  
  <p>The question: What am I missing here?</p>