∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E}
  (h : A ≤ B), A.relfinrank B = Module.finrank ↥A ↥(IntermediateField.extendScalars h)