coq - 「リライト[含意のある仮説]」の使い方

Question

CIS 500 Software Foundations course CIS 500 Software Foundations course . 現在MoreCoqにいます。の部分がわかりませんrewrite IHl1。それはどのように機能していますか？以前に使用したときにこれが機能しないのはなぜsimplですか?

Definition split_combine_statement : Prop := forall X Y (l1 : list X) (l2 : list Y),
  length l1 = length l2 -> 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.