I've found myself in a situation where I need to prove a PBW theorem for a certain quotient of an algebra $A/I$ where $A$ is a filtered algebra given by generators and relations. Furthermore $A$ has a PBW theorem in the sense that $grA \cong U(\mathfrak{g})$ for some infinite dimensional Lie algebra $\mathfrak{g}$.(For the people familiar $\mathfrak{g}$ is the twisted current algebra but I'm hoping that this won't matter). When trying to prove this I stumbled across Bergman's Lemma which I'm hoping to use. My plan essentially involved finding a suitable reduction system for $A$ showing that it has the right irreducibles (i.e the ones giving a PBW basis for $A$) and hence by Bergman's Lemma all ambiguities would be resolvable. This would save me from having to check that all ambiguities appearing in the reduction system for $A$ are resolvable,which seems close to impossible as unfortunately the presentation of $A$ is quite horrible. Now in my setting the ideal $I$ is generated by a single generator $x \in A$ so that I hopefully should be able to check the ambiguities in the reduction system where I just add the relation $x=0$ are resolvable. By Bergman's Lemma this would then be enough as I can already show that the irreducibles in that system contain a spanning set for $A/I$. The trouble I'm having is that I can't find a suitable reduction system for $A$ to begin with as I can't really compute what the irreducibles are (again owing to the fact that the presentation for $A$ is horrible).
However by Bergman's Lemma the existence of such a system is equivalent to the PBW theorem so it must be possible to write one down. I was wondering if there actually is a constructive way of doing so? I checked the literature but couldn't find anything and would appreciate any input. Otherwise I would also be interested in any other ideas of somehow proving a PBW theorem for $A/I$ based off the information I've given.