replaced "by simp" to close transitive chains with more standard "."