title: How to split equality of two lists?
body: <p>I have the following goal and context:</p>
  <pre><code>  A : Type
    eqb : A -&gt; A -&gt; bool
    H : forall a1 a2 : A, eqb a1 a2 = true &lt;-&gt; a1 = a2
    x : A
    l1' : list A
    IHl1' : forall l2 : list A, eqb_list eqb l1' l2 = true &lt;-&gt; l1' = l2
    y : A
    l2' : list A
    IHl2' : eqb_list eqb (x :: l1') l2' = true &lt;-&gt; x :: l1' = l2'
    H0 : x = y
    H1 : l1' = l2'
    ============================
    x :: l1' = y :: l2'
  </code></pre>
  <p>Is there a tactic that allows me to apply <code>H0</code> and <code>H1</code> and complete this proof?</p>
  <p>Thanks</p>