Do we need this? Formula is an abbrev for BoundedFormula, so BoundedFormula.iSup/BoundedFormula.iInf does everything you new definitions already do (and your new definitions aren't abbrevs)

I don't know. Personally I think that the current BoundedFormula and Formula duplication is quite annoying but so far we do seem to have been duplicating a lot of things (but the library is not completely consistent). BoundedFormula can be a bit anooying to use when reasoning about semantics because for a BoundedFormula L α 0 you have this term Fin 0 -> M at the end when you use BoundedFormula.realize which are always equal obviously, but not necessarily definitionally equal.

The best long term solution in my view is probably to claim that BoundedFormula is just an implementation detail and we should basically always be using Formula and we just have to introduce a single variable all and ex on formulas and the exact type of these definitions I'm not sure of. I don't have a strong opinion on any temporary fix before that.

I agree that there's some major cleanup that needs to happen in the long term - I wish I had a concrete suggestion for how it should go.

In the meantime, do you have a use case for iSup or iInf for Formulas as opposed to BoundedFormulas? Is it possible that we could even remove the BoundedFormula version and just work with Formulas now?

I'm personally fine having both if there's actual code that works better that way while awaiting a good general solution to duplication.

I almost never used BoundedFormula, I think mainly because I was very rarely quantifying over a single variable, it was always over an arbitrary finite number of variables.

A use case for iInf is the statement of Ax Grothendieck. It's about injectivity and surjectivity of maps K^n -> K^n and I needed iInf to state equality of elements of K^n