Update Contribution Guidelines

.github/pull_request_template.md

@@ -3,6 +3,10 @@
 * Ensure your PR follows the [contribution
   guidelines](https://github.com/leanprover/LNSym/blob/main/CONTRIBUTING.md).
 
+* Be mindful of the **no nonterminal simp** rule in your proofs.
+
+* Do not introduce any new external dependencies.
+
 * Remember to document and comment your code.
 
 * Note that before a PR to the `main` branch can be merged:

CONTRIBUTING.md

@@ -9,6 +9,16 @@ document before submitting any pull requests or issues.
 **Focused Changes**: Create small, focused PRs that address a single
 issue or implement a specific feature.
 
+**Maintainable Proofs**: Write your proofs in a maintainable way, even
+if doing so causes them to become more verbose. LNSym follows the
+***no nonterminal `simp`*** rule, which says that unless `simp` is
+closing the goal, it should always be converted to a `simp only [X, Y,
+Z]` call.
+
+**External Dependencies**: Do not introduce any new external
+dependencies into LNSym's codebase -- be mindful of what you
+import. Exceptions are possible, but only when absolutely necessary.
+
 **Documentation**: Add relevant documentation and comments to your
 code.