Commit 2022-11-24 10:55 5fce1791
View on Github →feat(logic/function/basic): refine extend_apply (#16944)
Add function.extend_apply_of_unique
which allows to rewrite function.extend f g e (f a) = g a
not only when f is injective, what function.extend_apply does,
but when f a = f b → g a = g b.
Generalize a few similar lemmas in the same way.
TODO ? : rewrite function.extend_apply to use this function.