Theorem Function.Injective.extend_apply

Modification history