Proved the ascii-art improved version of find_subtree_impl_kpl_app.
Added a so-far unused admitted lemma: appears_in_tree_when_appears_in_subtree_and_found.
Merge branch 'master' of github.com:nicolaidahl/BPlusTrees
Added a few exfalso before omega, because apparently I run a older version of Coq where omega needs a exfalso to work properly.