{K : Type u_1} →
  [inst : Field K] →
    (v : Valuation K (WithZero (Multiplicative ℤ))) →
      (L : Type u_2) →
        [inst_1 : Field L] →
          [inst_2 : Algebra K L] →
            (E : Type u_3) →
              [inst_3 : Field E] →
                [inst_4 : Algebra K E] →
                  [inst_5 : Algebra L E] →
                    [IsScalarTower K L E] →
                      Algebra ↥(integralClosure (↥v.valuationSubring) L) ↥(integralClosure (↥v.valuationSubring) E)