src/ZF/Perm.thy

 val id_inj = thm "id_inj";
 val id_surj = thm "id_surj";
 val id_bij = thm "id_bij";
 val subset_iff_id = thm "subset_iff_id";
 val inj_converse_fun = thm "inj_converse_fun";
-val left_inverse_lemma = thm "left_inverse_lemma";
 val left_inverse = thm "left_inverse";
 val left_inverse_bij = thm "left_inverse_bij";
-val right_inverse_lemma = thm "right_inverse_lemma";
 val right_inverse = thm "right_inverse";
 val right_inverse_bij = thm "right_inverse_bij";
 val inj_converse_inj = thm "inj_converse_inj";
 val inj_converse_surj = thm "inj_converse_surj";
 val bij_converse_bij = thm "bij_converse_bij";