title: renaming part of hypothesis in Coq
body: <p>After destructing n in my proof, I am stuck at the following:</p>
  
  <pre><code>1 subgoal
  n : nat
  X : Type
  h : X
  t : list X
  n' : nat
  E : n = S n'
  H' : length t = n'
  IHl : length t = n -&gt; nth_error t n = None
  ______________________________________(1/1)
  nth_error t n' = None
  </code></pre>
  
  <p>I want to rewrite using IHl, but that is not possible. How do I compose IHl and H' to make sense and prove this theorem?</p>