Theorem contractLeft_apply

Modification history