[FEAT] Tackle impossible cases with minimal requirements

[Stevengre]

In #888, we use ensure (0 ==Int #lookupDiscrAux(discriminant(0) discriminant(1) .Discriminants, ?SplHasDelegateKey) orBool 1 ==Int #lookupDiscrAux(discriminant(0) discriminant(1) .Discriminants, ?SplHasDelegateKey)) to avoid unreachable cases.

However, 0 <=Int ?SplHasDelegateKey andBool ?SplHasDelegateKey <=Int 1 and the definiton of #lookupDiscrAux should already give enough information that it should be 0 or 1 for this #lookupDiscrAux.

Could we provide a way to avoid this redundant ensure clause?