Remove a natural language tactic

Discussion on
https://github.com/JasonGross/HoTT/commit/7f6d4cfe2c0213e83cd3486286ca1ff1e7e4b1dd:

spitters added a note 7 hours ago
Why this pun ?

JasonGross added a note 2 hours ago
I figured that anyone wanting to mirror proofs in the book ~verbatim
might appreciate this tactic, (or maybe it should be Tactic Notation
"Since" "the" "goal" "is" "a" "mere" "proposition," "we" "may" "strip"
"truncations"). I could probably get it even closer, if there's actually
an interest here, so that you could write Since our goal is a mere
proposition, we may assume given a : A and H : P a. and have it find a
truncated thing of type { a : A | P a} and give you back a hypothesis a
: A and a hypothesis H : P a.

Bas Spitters
But why experiment with natural language only in an isolated place ?
Don't you think that one experiment (HoTT) is enough ?

JasonGross added a note 16 minutes ago
I think I was actually originally going to call it the longer name, and
later shortened it, but figured I'd leave in the longer one as well.

HoTT might be enough of an experiment, though I tend to like
experimenting with everything I can. Shall I go remove the pun? (It
doesn't matter much either way to me.)

spitters added a note 15 minutes ago
I prefer somewhat controlled experiments :-)