{u : Lean.Level} →
  {α : Q(Type u)} →
    (sα : Q(CommSemiring «$α»)) →
      (b a : Q(«$α»)) →
        (motive : (e' : Q(«$α»)) × Q(«$a» + «$b» = «$e'») → Sort u_1) →
          (x : (e' : Q(«$α»)) × Q(«$a» + «$b» = «$e'»)) →
            ((c : Q(«$α»)) → (pc : Q(«$a» + «$b» = «$c»)) → motive ⟨c, pc⟩) → motive x