{motive : Mathlib.Tactic.ITauto.AndKind → Sort u} →
  (ctorIdx : ℕ) →
    (t : Mathlib.Tactic.ITauto.AndKind) →
      ctorIdx = t.ctorIdx → Mathlib.Tactic.ITauto.AndKind.ctorElimType ctorIdx → motive t