We typically use the _1 and _2 suffix to denote individual directions
of a lemmas that is a biimplication.