∀ (R : Type u_2) (M : Type u_1) [inst : Monoid R] [inst_1 : AddCommMonoid M] [inst_2 : DistribMulAction R M]
  (x y : { v // v ≠ 0 }) (motive : (MulAction.orbitRel Rˣ M) ↑x ↑y → Prop) (h : (MulAction.orbitRel Rˣ M) ↑x ↑y),
  (∀ (a : Rˣ) (ha : (fun m => m • ↑y) a = ↑x), motive ⋯) → motive h