base_logic/lib/gset_bij: fix gset_bij_own_elem_agree; add gset_bij_own_elem_auth_agree

This MR fixes lemma gset_bij_own_elem_agree (removing the spurious argument L) and adds a new lemma gset_bij_own_elem_auth_agree that allows to gain knowledge about an element being in the bijection and that seems to be missing from the lemmas in the library (please correct me if I'm wrong and there's an easy way to obtain this with the present lemmas without unsealing).