Commit 2021-03-25 10:59 879273e8

feat(logic/basic, logic/function/basic): make cast the simp-normal form of eq.mp and eq.mpr, add lemmas (#6834) This adds the fact that eq.rec, eq.mp, eq.mpr, and cast are bijective, as well as some simp lemmas that follow from their injectivity.