Prepare for release

Update gitignore

Shorten proof

Update README

Bump version to 1.2

.gitignore

@@ -7,3 +7,4 @@ auto/*
 **/*.olean
 /_target
 /leanpkg.path
+test.org

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

leanpkg.toml

@@ -1,6 +1,6 @@
 [package]
 name = "flypitch"
-version = "1.1"
+version = "1.2"
 lean_version = "3.4.2"
 path = "src"
 

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