diff --git a/Duper/Interface.lean b/Duper/Interface.lean
index f166678..4c46769 100644
--- a/Duper/Interface.lean
+++ b/Duper/Interface.lean
@@ -418,7 +418,7 @@ partial def getLeavesFromDTr (t : Auto.DTr) : Array String :=
     track of `isFromGoal` information through the monomorphization procedure. -/
 def formulasToAutoLemmas (formulas : List (Expr × Expr × Array Name × Bool)) : MetaM (Array Auto.Lemma) :=
   formulas.toArray.mapM
-    (fun (fact, proof, params, isFromGoal) => -- For now, isFromGoal is ignored
+    (fun (fact, proof, params, isFromGoal) =>
       return {proof := ← Meta.mkAppM ``of_eq_true #[proof], type := fact, params := params, deriv := (.leaf s!"{isFromGoal}")})
 
 /-- Converts formulas/lemmas from the format used by Auto to the format used by Duper. -/
diff --git a/README.md b/README.md
index 9926177..a0c0c67 100644
--- a/README.md
+++ b/README.md
@@ -7,7 +7,7 @@ Duper is an automatic proof-producing theorem prover broadly similar to Isabelle
 To use Duper in an existing Lean 4 project, first add this package as a dependency. In your lakefile.lean, add:
 
 ```lean
-require Duper from git "https://github.com/leanprover-community/duper.git" @ "v0.0.10"
+require Duper from git "https://github.com/leanprover-community/duper.git" @ "v0.0.11"
 ```
 
 Then, make sure that your `lean-toolchain` file contains the same version of Lean 4 as Duper and that if your project imports [std4](https://github.com/leanprover/std4.git), then it uses the same version of std4 as the Duper branch of [Auto](https://github.com/leanprover-community/lean-auto.git). This step is necessary because Duper depends on Auto which depends on std4, so errors can arise if your project attempts to import a version of std4 different from the one imported by Duper.