This tactic applies contract_centric with evars and puts the "establish
facts" obligation last. This allows the user to instantiate these during
the proof of the property.