Theorem Set.piCongrLeft_comp_restrict

Modification history