{R : Type u} →
  {M : Type v} →
    [inst : VAdd R M] →
      {motive : SubAddAction R M → Sort u_1} →
        (t : SubAddAction R M) →
          ((carrier : Set M) →
              (vadd_mem' : ∀ (c : R) {x : M}, x ∈ carrier → c +ᵥ x ∈ carrier) →
                motive { carrier := carrier, vadd_mem' := vadd_mem' }) →
            motive t