Commit 2022-04-03 04:50 955e95ad

feat(logic/function/basic): add some more API for injective2 (#13074) Note that the new .left and .right lemmas are weaker than the original ones, but the original lemmas were pretty much useless anyway, as hf.left h was the same as (hf h).left.