Theorem Equiv.prodCongrLeft_apply

Modification history