various

- prover abduces (very simple) lvar instantiations
- implies_triple is more robust with respect to lvar instantiations
  (which is why infer_test/test18 terminates now)