Proof of dist_hom_over_mset_for