{R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {motive : Algebra.Extension R S → Sort u_1} →
            (t : Algebra.Extension R S) →
              ((Ring : Type w) →
                  [commRing : CommRing Ring] →
                    [algebra₁ : Algebra R Ring] →
                      [algebra₂ : Algebra Ring S] →
                        [isScalarTower : IsScalarTower R Ring S] →
                          (σ : S → Ring) →
                            (algebraMap_σ : ∀ (x : S), (algebraMap Ring S) (σ x) = x) →
                              motive
                                { Ring := Ring, commRing := commRing, algebra₁ := algebra₁, algebra₂ := algebra₂,
                                  isScalarTower := isScalarTower, σ := σ, algebraMap_σ := algebraMap_σ }) →
                motive t