Support for mutual and nested inductive types as `DecidableEq` instance generator

[leodemoura]

We currently have to manually write DecidableEq instances for nested and mutual inductive datatypes. Here is an example.

namespace Example

inductive Min where
  | Base
  | Const (a : List Min)

mutual
def decMin (a b : Min) : Decidable (a = b) :=
  match a, b with
  | .Base, .Base         => isTrue rfl
  | .Base, .Const ..     => isFalse (by intro; contradiction)
  | .Const .., .Base     => isFalse (by intro; contradiction)
  | .Const as, .Const bs => match decMinList as bs with
    | isTrue h => isTrue (by rw [h])
    | isFalse _ => isFalse (by intro h; injection h; contradiction)

def decMinList (as bs : List Min) : Decidable (as = bs) :=
  match as, bs with
  | [], [] => isTrue rfl
  | _::_, [] => isFalse (by intro; contradiction)
  | [], _::_ => isFalse (by intro; contradiction)
  | a::as, b::bs =>
    match decMin a b with
    | isTrue h₁ => match decMinList as bs with
      | isTrue h₂ => isTrue (by rw [h₁, h₂])
      | isFalse _ => isFalse (by intro h; injection h; contradiction)
    | isFalse _ => isFalse (by intro h; injection h; contradiction)
end

instance : DecidableEq Min :=
  decMin