∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {A B : Subalgebra R S}
  [Subsingleton S], (Subalgebra.toSubmodule A).LinearDisjoint (Subalgebra.toSubmodule B) = True