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.

Beluga/examples/literate_beluga/2Advanced/Weak_Normalization.bel

Line 157 in 1d39095

rec main : {g:ctx}{M:[g |- tm A[]]} RedSub [g] [ |- $S[^]] -> Reduce [|- A] [ |- M[$S]] =

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) /