Change 'expl' attribute for generated invariants

[Lysxia]

Invariants obtained by desugaring for loops and mutation of types with invariants in loops are annotated with something different than "loop invariant".

I tried to fix the span for the former kind of invariants to the for keyword, but right now they still point to the user-annotated invariant attribute. Any idea where that span is being set?

• fix spans for "for invariants"
• find a better name than "proph invariant"
• update test suite