sum.lex.inl_mono source