{motive : Batteries.Tactic.Alias.AliasInfo → Sort u} →
  (t : Batteries.Tactic.Alias.AliasInfo) →
    t.ctorIdx = 1 → ((n : Lean.Name) → motive (Batteries.Tactic.Alias.AliasInfo.forward n)) → motive t