ack + typo

1 files changed, 4 insertions, 1 deletions

diff --git a/README.md b/README.md
index 1ec24e4..efb2e91 100644
--- a/README.md
+++ b/README.md
@@ -56,7 +56,7 @@ without the system interpreting them as axioms:
 by {Taut};
 ```
 
-Second, if you prove some claim directly from an earlier claim, you can alway
+Second, if you prove some claim directly from an earlier claim, you can always
 introduce the implication of the two claims (which now no longer depends on the
 earlier claim):
 ```
@@ -188,3 +188,6 @@ above.
   The main concern is the `{Generalize}` pseudo-claim and how it determines
   which variables we can generalize (maybe we need to do better tracking of
   assumption discharging).
+
+## Thanks
+Thanks David K Zhang for very helpful conversations.