title: How can I prove equality of lists by induction?
body: <p>I'm very new to Coq. Suppose under some hypothesis I want to prove <code>l1 = l2</code>, both of which are lists. I wonder what is a general strategy if I want to prove it inductively.</p>
  
  <p>I don't know of any way to do induction on <code>l1</code> and <code>l2</code> at the same time. If I do induction first on <code>l1</code>, then I'll end up having to prove <code>l1 = l2</code> under hypothesis <code>t1 = l2</code>, where <code>t1</code> is tail of <code>l1</code>, which is obviously false.</p>