generalize lemma-insert-same to arbitrary Setoids