{motive_6 : Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof → Sort u} →
  (t : Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof) →
    t.ctorIdx = 0 → ((h : Lean.FVarId) → motive_6 (Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof.dec h)) → motive_6 t