generic definitions of inductive grammars

[maxsnew]

Experimenting with a general inductive grammar defined as a least fixed point of a syntactically described functor. This does have to use the {-# TERMINATING #-} pragma because the termination checker isn't convinced but it looks totally benign to me.

Starting this as a draft so @stschaef can take a look at the non-indexed version before I get to the indexed version. Things to discuss would be the naming and whether we should make the universe levels more general

[stschaef]

I'm experimenting a bit locally with the definitions in Inductive to see how we might implement Kleene star via these definitions. It seems that we want better universe polymorphism to avoid lifts at the call sight

I'm sketching something up and will post in a minute

[stschaef]

LGTM just synced with the incoming opaqueness of tensor in main. Passes locally, will merge after the CI runs