Skip to content

Rename elim and intro lemmas

I have identified (all) faulty intro/elim lemmas and renamed them to their counterpart. Most changes are due to applications, hence look out for lines with Definition or Lemma.

In my opinion, the old names of the changed lemmas were misleading, but some lemmas might also better be renamed differently instead. At the moment I have just swapped the names to have them show up in the MR.

Merge request reports

Loading