diff --git a/Doc/pics/Logo.bmp b/Doc/pics/Logo.bmp
index 9c30e0d..3098fa6 100644
Binary files a/Doc/pics/Logo.bmp and b/Doc/pics/Logo.bmp differ
diff --git a/README.md b/README.md
index c6083f7..a1f2396 100644
--- a/README.md
+++ b/README.md
@@ -1,4 +1,6 @@
-
+
+ 
+
Type **"auto 👍"** to see whether auto is set up.
@@ -6,7 +8,9 @@ Type **"auto 👍"** to see whether auto is set up.
Lean-auto is an interface between Lean and automated theorem provers, 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):
-
+
+
+
## Usage
* ``auto [,*] u[,*] d[,*]``