Better tactic for scoping proofs #7
Description
Currently there is a really basic auto tactic in Utils.Tactics, but it would be really nice if we could have a tactic that automatically constructs proofs of separation, subscoping, and elementhood using the combinators provided by the library.