The tactic "injection' H" now uses the name "H" for the first hypothesis it
generates. Fresh names will still be used for the remaining hypotheses.