diff --git a/.gitignore b/.gitignore
index dcfd511..015571c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -7,3 +7,4 @@ auto/*
 **/*.olean
 /_target
 /leanpkg.path
+test.org
\ No newline at end of file
diff --git a/README.org b/README.org
index 4dd59b7..1d48d4f 100644
--- a/README.org
+++ b/README.org
@@ -14,7 +14,7 @@ leanpkg build
 
 This will additionally compile the requisite parts of ~mathlib~, and will take multiple minutes.
 
-Optionally, you can install the ~update-mathlib~ script (see [[https://github.com/leanprover-community/mathlib/blob/master/docs/install/linux.md][here]] for instructions) which will download pre-built ~.olean~ files, considerably speeding up the compilation time. In this case, you can instead run
+Optionally, you can install the ~update-mathlib~ script (see [[https://github.com/leanprover-community/mathlib/blob/master/docs/install/linux.md][here]] for instructions) which will download pre-built ~.olean~ files, considerably speeding up the compilation. In this case, you can instead run
 #+BEGIN_SRC
 leanpkg configure
 update-mathlib
diff --git a/leanpkg.toml b/leanpkg.toml
index 041889f..8d54e6e 100644
--- a/leanpkg.toml
+++ b/leanpkg.toml
@@ -1,6 +1,6 @@
 [package]
 name = "flypitch"
-version = "1.1"
+version = "1.2"
 lean_version = "3.4.2"
 path = "src"
 
diff --git a/src/bvm_extras.lean b/src/bvm_extras.lean
index d494016..9f6f402 100644
--- a/src/bvm_extras.lean
+++ b/src/bvm_extras.lean
@@ -598,8 +598,7 @@ begin
  have : Γ ≤ w ⊆ᴮ x,
    by {rw[subset_unfold'], bv_intro w', bv_imp_intro,
        have := mem_of_mem_subset a_left_right H,
-       apply mem_of_mem_subset, show bSet 𝔹, from y,
-       apply subset_of_mem_transitive ‹_› ‹_›, from ‹_›},
+       from mem_of_mem_subset (subset_of_mem_transitive ‹_› ‹_›) ‹_›},
  from H_right w ‹_› ‹_›}
 end