Added theorem about excaption names being distinct

And put it next to type_sound_inv_dup_ctors in the calls to metis_tac in
the proof.