update readme again

README.md

@@ -1,17 +1,19 @@
 <p align="center">
   <img src="Doc/pics/Logo.bmp" width="600" />
 </p>
-
-Type **"auto 👍"** to see whether auto is set up.  
-
+
 Lean-auto is an interface between Lean and automated theorem provers. Up to now, lean-auto is maintained and developed primarily by Yicheng Qian (GitHub: PratherConid). It is currently in active development, and pull requests/issues are welcome. For more information, feel free to reach out to Yicheng Qian on [Lean Zulip](https://leanprover.zulipchat.com).  
-Lean-auto is based on a monomorphization procedure from dependent type theory to higher-order logic and a deep embedding of higher-order logic into dependent type theory. It is capable of handling dependently-typed and/or universe-polymorphic input terms. Currently, proof reconstruction can be handled by [Duper](https://github.com/leanprover-community/duper), a higher-order superposition prover written in Lean.  
+
+Lean-auto is based on a monomorphization procedure from dependent type theory to higher-order logic and a deep embedding of higher-order logic into dependent type theory. It is capable of handling dependently-typed and/or universe-polymorphic input terms. Currently, proof reconstruction can be handled by [Duper](https://github.com/leanprover-community/duper), a higher-order superposition prover written in Lean.
+
 Lean-auto is still under development, but it's already able to solve nontrivial problems. For example the first part of the "snake lemma" in category theory can be solved by a direct invocation to ``auto`` (and the second part can also be partly automated):
 
 <p align="center">
   <img src="Doc/pics/shortfive.png" alt="drawing" width="500"/>
 </p>
 
+Type **"auto 👍"** to see whether auto is set up.  
+
 ## Usage
 * ``auto [<term>,*] u[<ident>,*] d[<ident>,*]``
   * ``u[<ident>,*]``: Unfold identifiers