Lemmas for the mono tactic

The mono tactic works by throwing all lemmas tagged with the attribute @[mono] at the goal. In this file we tag a few foundational lemmas with the mono attribute. Lemmas in more advanced files are tagged in place.