Theorem congr_fun₃

Modification history