{motive : Lean.Elab.WF.GuessLex.MutualMeasure → Sort u} →
  (t : Lean.Elab.WF.GuessLex.MutualMeasure) →
    ((a : Array ℕ) → motive (Lean.Elab.WF.GuessLex.MutualMeasure.args a)) →
      ((a : ℕ) → motive (Lean.Elab.WF.GuessLex.MutualMeasure.func a)) → motive t