Induction on list

Stream: general

[Yury G. Kudryashov]

Can I emulate the following equation compiler induction

theorem mythm : ∀ (l : list α), p l
| [] := p0
| [a] := p1
| (a::b::l) := p2 (mythm l)

using induction tactic? Or should I add a lemma list.induction_on2 : ∀ l, C [] → C [a] → (∀ a b l, C l → C (a::b::l)) → C l?

[Yury G. Kudryashov]

In my specific example I get l as a result of rcases so I can't use equation compiler directly (or I don't know how to do it).

[Mario Carneiro]

You could do strong induction on the length of the list