title: Using "rewrite [hypothesis with implication]"
body: <p>Working through CIS 500 Software Foundations course<a href="http://www.seas.upenn.edu/~cis500/current/index.html" rel="nofollow">CIS 500 Software Foundations course</a>. Currently on <a href="http://www.seas.upenn.edu/~cis500/current/sf/MoreCoq.v" rel="nofollow">MoreCoq</a>. I don't understand the <code>rewrite IHl1</code> part. How is it working? Why does this not work when used before <code>simpl</code>?</p>
  
  <pre><code>Definition split_combine_statement : Prop := forall X Y (l1 : list X) (l2 : list Y),
    length l1 = length l2 -&gt; split (combine l1 l2) = (l1,l2).
  
  Theorem split_combine : split_combine_statement.
  Proof. unfold split_combine_statement. intros. generalize dependent Y. induction l1. 
   Case "l = []". simpl. intros. destruct l2. 
    SCase "l2 = []". reflexivity. 
    SCase "l2 = y :: l2". inversion H.
   Case "l = x :: l1". intros.  destruct l2. 
    SCase "l2 = []". inversion H.
    SCase "l2 = y :: l2". simpl. rewrite IHl1.
  </code></pre>