{R : Type u_1} →
  [inst : Add R] →
    [inst_1 : Mul R] →
      {motive : RingCon R → Sort u} →
        (t : RingCon R) →
          ((toCon : Con R) →
              (add' : ∀ {w x y z : R}, toCon.toSetoid w x → toCon.toSetoid y z → toCon.toSetoid (w + y) (x + z)) →
                motive { toCon := toCon, add' := add' }) →
            motive t