pruned some auxiliary lemmas in RC

removed some lemmas from file RezkCompletion/auxiliary_lemmas_HoTT.v

the remaining lemmas in that file are mostly about path space of a sigma type and will be moved to Foundations in a forthcoming pull request