(motive : Lean.Elab.Info → Sort u_1) →
  (i : Lean.Elab.Info) →
    ((ti : Lean.Elab.TermInfo) → motive (Lean.Elab.Info.ofTermInfo ti)) →
      ((fi : Lean.Elab.FieldInfo) → motive (Lean.Elab.Info.ofFieldInfo fi)) →
        ((x : Lean.Elab.Info) → motive x) → motive i