Add and prove imp_not_{l,r}_{and,or}_equiv,
              not_imp_not_{l,r}_{and,or}_equiv.

Function_compl:
Add and prove surj_can_uniq_r, inj_contra_{rev,equiv}.

Function_sub:
Add and prove imS_dec,
              injS_id, injS_contra{,_rev,_equiv}, injS_equiv,
              injS_canS_uniq_l, comp_injS_r, surjS_canS_uniq_r,
              injS_has_left_inv.