Commit 2024-02-22 15:18 7bb1f49e
View on Github →feat: Dependent eliminator for Fin 0 (#10850)
Fin.elim0 and Fin.elim0' are exactly the same function (non-dependent eliminator for Fin 0) and we were missing the dependent version (I suspect that Fin.elim0 originally was dependent, and became non-dependent upon landing in Std).
From PFR