{R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : ValuativeRel R] →
      [inst_2 : Preorder R] →
        {motive : ValuativePreorder R → Sort u} →
          ((vle_iff_le : ∀ (x y : R), x ≤ᵥ y ↔ x ≤ y) → motive ⋯) → (t : ValuativePreorder R) → motive t