feat(?): Better support for prod in well_founded

[eric-wieser]

This is an attempt at following up on https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Well.20founded.20definition/near/205105727, which noted that the following didn't work without extra encouragement:

def test : list ℕ × list ℕ → list ℕ × list ℕ
| ([],m) := ([],m)
| (a::l,m) := test(l,m)
-- works with
-- using_well_founded {dec_tac := `[apply prod.lex.left, well_founded_tactics.default_dec_tac]}

I have no idea how to test this locally, unfortunately.

If you think this concept is flawed, feel free to close.

[gebner]

The current plan is actually to remove this file altogether, @bryangingechen has started here: #288