[Prover.is_entailment] doesn't allow instantiations anymore

note
 - instantiations are desirable when comparing lvars from different scopes
 - instantiations are undesirable when comparing lvars from the same scope

e.g.:
 - state (from confgraph) and precondition (from triple) -> instantiate
 - pre (from triple) and pre (from other triple) -> instantiate
 - sate (from confgraph) and state (from same confgraph) -> do NOT