Add is_closed_term tactic

This MR adds a tactic that has been proven quite useful in RefinedC. An example usecase can be found here: https://gitlab.mpi-sws.org/iris/stdpp/-/blob/4168f736be2fd735dc9680fda0a3b3a6af2b1b5e/theories/bitvector.v#L294 (There it is still called checked_closed).

tests/is_closed_term.ref

+"is_closed_term_test"
+     : string
+The command has indeed failed with message:
+Tactic failure: The term x is not closed.
+The command has indeed failed with message:
+Tactic failure: The term (x + 1) is not closed.
+The command has indeed failed with message:
+Tactic failure: The term (x + y) is not closed.
+The command has indeed failed with message:
+Tactic failure: The term section_variable is not closed.
+The command has indeed failed with message:
+Tactic failure: The term (section_variable + 1) is not closed.