I am ok with the pull request, although I'd probably avoid the "mini tactic" style of writing proofs, such as this one.