∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M),
  CliffordAlgebra.toEven Q =
    (CliffordAlgebra.lift Q)
      ⟨LinearMap.codRestrict (CliffordAlgebra.evenOdd (CliffordAlgebra.EquivEven.Q' Q) 0)
          (LinearMap.mulLeft R (CliffordAlgebra.EquivEven.e0 Q) ∘ₗ CliffordAlgebra.EquivEven.v Q) ⋯,
        ⋯⟩