- A `Match from num is translated to pure by masking branches
with underscore lambdas
- The eating step on the divergent does not create a substitution in sigma
(to be understood...)
- In the branch of matches, \_. !divergent is translated to delta
- The checks in dangerous must still be fixed to go under lambdas