Refactored the code for overflow to the normal child into a seperate lemma.
Everything to do with nodes in insert'_impl_appears now works. Still cases left with leafs.
Merge branch 'master' of github.com:nicolaidahl/BPlusTrees
Added a exfalso to remain compatibile with older Coq versions.
Adjusted the insert'_impl_appears_overflow_* proofs to meet new requirements for cut_list_right_elim.