the strategy seems to be fixed (ie. does not imply those strange Lang.floats non-initialized context exceptions)

ast modifs and additional arrow_taint phase to retrieve which arrow "protects" / "taints" which variable

stronger strategy that can unify a transition hypothesis with a sub-term under existentials, and unfold memory packs also

add a custom strategy to try to unfold and find witnesses automatically for transition relations in WP