Merge pull request #6 from BoltonBailey/patch-1

Update README.md to capitalize Duper in require

README.md

@@ -7,7 +7,7 @@ Duper is an automatic proof-producing theorem prover broadly similar to Isabelle
 To use Duper in an existing Lean 4 project, first add this package as a dependency. In your lakefile.lean, add:
 
 ```lean
-require duper from git "https://github.com/leanprover-community/duper.git" @ "v0.0.5"
+require Duper from git "https://github.com/leanprover-community/duper.git" @ "v0.0.5"
 ```
 
 Then, make sure that your `lean-toolchain` file contains the same version of Lean 4 as Duper and that if your project imports [std4](https://github.com/leanprover/std4.git), then it uses the same version of std4 as the Duper branch of [Auto](https://github.com/leanprover-community/lean-auto.git). This step is necessary because Duper depends on Auto which depends on std4, so errors can arise if your project attempts to import a version of std4 different from the one imported by Duper.
@@ -73,4 +73,4 @@ If Duper saturates, meaning Duper fully processed all clauses and was unable to
 
 If Duper successfully proves the goal and you want to obtain additional information about the proof Duper found, then `set_option trace.duper.printProof true` will show the clauses used in the final proof and `set_option trace.duper.proofReconstruction true` will show information about the proofs of said clauses and the final proof that was used to resolve the goal.
 
-In our experience, we have generally found attempting to debug problems that Duper saturates on to be more fruitful than problems that Duper timed out on (because there is typically a smaller volume of clauses to look at). This is most helpful when Duper is capable of solving a problem in principle but needs to be provided some additional fact that it is not natively aware of. Additionally, we have generally found trace output to be more readable when preprocessing is disabled, since the current preprocessing procedure transforms input lemmas into facts with uninformative names. If you need to look at Duper's trace output even with preprocessing enabled, then `set_option trace.duper.monomorphization.debug true` will cause Duper to print its input facts before and after the monomorphization procedure. This can help in understanding how the monomorphized constants that appear in Duper's clauses correspond to constants in the original problem.
+In our experience, we have generally found attempting to debug problems that Duper saturates on to be more fruitful than problems that Duper timed out on (because there is typically a smaller volume of clauses to look at). This is most helpful when Duper is capable of solving a problem in principle but needs to be provided some additional fact that it is not natively aware of. Additionally, we have generally found trace output to be more readable when preprocessing is disabled, since the current preprocessing procedure transforms input lemmas into facts with uninformative names. If you need to look at Duper's trace output even with preprocessing enabled, then `set_option trace.duper.monomorphization.debug true` will cause Duper to print its input facts before and after the monomorphization procedure. This can help in understanding how the monomorphized constants that appear in Duper's clauses correspond to constants in the original problem.