∀ {R : Type u_3} {M : Type u_1} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {A : Type u_2} [inst_3 : Ring A] [inst_4 : Algebra R A] (f : CliffordAlgebra.EvenHom Q A)
  (m : M) (acc : A × ↥(CliffordAlgebra.even.lift.S✝ f)),
  LinearMap.mulRight R acc.1 ∘ₗ f.bilin.flip m ∈
    ↑(Submodule.span R {f' | ∃ x m₂, f' = (LinearMap.lcomp R A (f.bilin.flip m₂)) (LinearMap.mulRight R x)})