∀ {R : Type u_1} {M : Type u_2} {P : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid P] [inst_4 : Module R P] {N : Submodule R P},
  N.FG →
    ∀ {x y : TensorProduct R (↥N) M},
      (LinearMap.rTensor M N.subtype) x = (LinearMap.rTensor M N.subtype) y →
        ∃ N',
          N'.FG ∧
            ∃ (h : N ≤ N'),
              (LinearMap.rTensor M (Submodule.inclusion h)) x = (LinearMap.rTensor M (Submodule.inclusion h)) y