Theorem Function.Involutive.exists_mem_and_apply_eq_iff

Modification history