{R : Type u} →
  [inst : Semiring R] →
    {motive : StrongRankCondition R → Sort u_1} →
      (t : StrongRankCondition R) →
        ((le_of_fin_injective : ∀ {n m : ℕ} (f : (Fin n → R) →ₗ[R] Fin m → R), Function.Injective ⇑f → n ≤ m) →
            motive ⋯) →
          motive t