forall a_0 m_1 n_2 . a_0 %(m_1 n_2) -> a_0