Can Lawson's proof (that the canonical inclusion into a Clifford algebra is injective) be fixed? The first proof in Lawson & Michelsohn's Spin Geometry is known to be wrong. The claim, which appears in a paragraph on page 8 (not in an official proposition), is that the projection map $\pi_q|_V:\mathscr T(V)\to \text{Cl}(V,q)$ is injective.
For completeness, here is their "proof." $(V,q)$ is a vector space with a quadratic form, $\mathscr T(V)$ is the tensor algebra over $V$, and $\mathscr J_q(V)$ is the ideal of $\mathscr T(V)$ generated by elements of the form $v\otimes v+q(v)1$.

We prove that $\pi_q|_V$ is injective as follows. We say that an element $\varphi\in\mathscr T(V)$ is of pure degree $s$ if $\varphi\in\bigotimes^sV$ . (Every element of $\mathscr T(V)$ is a finite sum of elements of pure degree.) We want to show that any element $\mathscr J_q(V)\cap V$ is zero. Any such element can be written as a finite sum $\varphi=\sum a_i\otimes(v_i\otimes v_i+q(v_i))\otimes b_i$ where we may assume that the $a_i$'s and $b_i$'s are of pure degree. Since $\varphi\in V=\bigotimes^1V$, we conclude that $\sum a_{i'}\otimes(v_{i'}\otimes v_{i'})\otimes b_{i'}=0$, where this sum is taken over those indices with $\deg a_i+\deg b_i$ maximal. This equation implies, by contraction with $q$, that $\sum a_{i'}q(v_{i'})b_{i'}=0$. Proceeding inductively, we prove that $\varphi=0$.

I don't know what they mean by "contraction with $q$," so I can't even tell how this proof is supposed to work, much less how it goes wrong. That said, I don't really care what they intended or what's wrong with it, but rather I'd like to have a correct version of this proof in the same "spirit" as was intended here.
A correct proof is given in the above-linked MO post, but it resorts to a representation of the Clifford algebra acting on the exterior algebra, which feels like a very different approach to me. We essentially need to show that the ideal $\mathscr J_q(V)$ is not equal to all of $\mathscr T(V)$, and I like the idea of showing this directly using the definition of $\mathscr J_q(V)$ and the structure of $\mathscr T(V)$, which I think is the approach that Lawson & Michelsohn were intending.
 A: $\def\kk{\Bbbk}$Let $V$ be a vector space, let $q:V\to\kk$ be a quadratic form on $V$, and let $C(V,q)$ be the corresponding Clifford algebra, which is the quotient of the tensor algebra $T(V)$ by the ideal $I$ generated by all elements of the form $v^2-q(v)1$.
Let us now suppose that the ground field $\kk$ is not of characteristic $2$. There is then a symmetric bilinear form $(-,-):V\times V\to\kk$ such that $q(v)=(v,v)$ for all $v\in V$, and the ideal $I$ is generated by all elements of the form $vw+wv-2(v,w)1$ with $v$ and $w$ in $V$.
In fact, since now the generators are bilinear, we can give a much smaller set of generators. Let $(x_1,\dots,x_n)$ be a basis of $V$. Then the set of elements $$x_ix_j+x_jx_i+2(x_i,x_j)1 \qquad 1\leq i\leq j\leq n$$  is enough to generate $I$.
We order the basis so that $x_1 < \cdots < x_n$, and extend this to a graded-lexicographic monomial ordering on the set of monomials in $T(V)$. We can turn the generating set we have into a rewriting system, with rules $$x_jx_i\leadsto -x_ix_j+2(x_i,x_j)1 \qquad 1\leq i\leq j\leq n.$$
This rewriting system has overlapping ambiguities of the form $x_kx_jx_i$, one for each choice of indices such that $k>j>i$, and it is easy to check that each of this ambiguities can be resolved. It follows from Bergman's Diamond Lemma that the quotient $T(V)/I$ has as basis the set of all monomials $x_{i_1}\cdots x_{i_r}$ with $1\leq i_1<i_2<\cdots<i_t\leq n$. These are the so called standard monomials with respect to the rewritig system described above, and obvious their number is $2^n$, as it should be.
In particular, the classes of the $n$ generators $x_1,\dots,x_n$ are linearly independent in $T(V)/I$ and therefore the canonical mal $V\to T(V)/I$ is injective. This does what we want.
—————
This proof is completely incomprehensible if one does not know how the Diamond Lemma works, of course. For that I refer to any introduction to noncommutative Gröbner bases, of which there are nowadays quite a few. Explaining that here would be too long for this margin.
The idea of the proof mentioned in the question is, more or less, what is behind the argument that the Diamond Lemma works. Making this precise does require some work and preparations.
The verification of the confluency of this rewriting system is much simpler than the one one needs to do when proving the PBW theorem for Lie algebras that I mentioned in the comments.
