Incorrect totality check for weak normalization example

[Lysxia]

In Weak_Normalization.bel, the main proof makes the term M decrease, but I can incorrectly claim that it is the context g that's decreasing.

https://github.com/Beluga-lang/Beluga/blob/1d39095c99dc255d972a339d447dc04286d8c13f/examples/literate_beluga/2Advanced/Weak_Normalization.bel#L157

i.e., Beluga accepts the / total g (main g _ _ _) / annotation when it shouldn't. (It does accept / total m (main _ _ _ m) / as well.)

rec main : {g:ctx}{M:[g |- tm A[]]} RedSub [g] [ |- $S[^]] -> Reduce [|- A] [ |- M[$S]] =
  / total g (main g _ _ m) /