Global Instance all_to_empty_isequiv, Lemma ex_falso added
if_not_hprop_then_equiv_Empty simplified
renamed
Merge pull request #555 from marcbezem/master

Final polish concerning #543