Theorem Function.LeftInverse.eq_rec_eq

Modification history