Module Wp.LetifySource

bind sigma defs xs select definitions in defs targeting variables xs. The result is a new substitution that potentially augment sigma with definitions for xs (and others).

add_definitions sigma defs xs ps keep all definitions of variables xs from sigma that comes from defs. They are added to ps.

Pruning strategy ; selects most occurring literals to split cases.