Update README.md

README.md

@@ -28,6 +28,6 @@ Please visit [LeanDojo Website](https://leandojo.org/) for details.
 
 The model's input consists of retrieved premises concatenated with the current proof state and truncated to 2300 UTF-8 bytes. 
 The proof state is formatted by Lean's pretty printer, the same as the input format of our [model w/o retrieval](https://huggingface.co/kaiyuy/leandojo-lean3-tacgen-byt5-small).
-Retrieved premises are in the form of Lean code, except that their fully qualified names (marked by `<a>...</a>` are used). Please see the example on the right. 
+Retrieved premises are in the form of Lean code, except that proofs are removed and fully qualified names (marked by `<a>...</a>`) are used. Please see the example on the right.