That extraction is what the term_variables/2 predicate does that I use in my code. It gives you a list of all unbound variables in the given term. To simulate t

That extraction is what the term_variables/2 predicate does that I use in my code. It gives you a list of all unbound variables in the given term. To simulate the quantification, I then just add that list in front of the term with the ^ operator (which has no semantics, it is just the traditional constructor for these things). So for `_G947 -> _G947` I get the variable list `[_G947]` and use it to represent the universally quantified term as `[_G947]^(_G947 -> _G947)`. If you want to display this with nicer variable names, just substitute names of your choice for the variables in the quantifier list.