diff --git a/formal.scm b/formal.scm
index 1eb57a2..ba1ec0d 100644
--- a/formal.scm
+++ b/formal.scm
@@ -205,12 +205,13 @@
               (return #f))))
       (proof-steps proof))
      (when (or (member #f prems) (premises<=? goals prems))
+       (printf "Proof complete!\n")
        (return #t))
-     (format #t "Unsolved goals:\n~{~a\n~}~{⊢ ~a\n~}\n"
-             prems (filter (lambda (g) (not (member g prems))) goals)))))
+     (printf "Unsolved goals:\n~{~a\n~}~{⊢ ~a\n~}\n"
+             (reverse prems)
+             (filter (lambda (g) (not (member g prems))) goals)))))
 
-;; TODO: i can just guess lol
-;; this really isn't far from the macroless version....
+;; TODO: this really isn't far from the macroless version....
 (define and-comm
   (proof (p q)
     (argument (p q)
@@ -228,3 +229,21 @@
     [p simplification]
     [q simplification]
     [(pand q p) conjunction]))
+
+;; TODO: make this expressible better 
+;; TODO: use proofs for other proofs nicely
+;; the mismatch between what is written and what is shown is hideous
+;; avoidable by being explicit ig
+(define and-assoc.inl 
+  (proof (p q r)
+    (argument (p q r)
+      [(pand p (pand q r))]
+      [(pand (pand p q) r)])
+    [p simplification]
+    [(pand q r) simplification]
+    [q simplification]
+    [r simplification]
+    [(pand p q) conjunction]
+    [(pand (pand p q) r) conjunction]))
+
+(proof-valid? and-assoc.inl)