Destruct patterns: Support -> and <- (at least) for pure Coq equalities, and maybe injection patterns

In lambdaRust, we sometimes write something like iDestruct "H" as "[? EQ]"; iDestruct "EQ" as %->. It would be nice if we could write iDestruct "H" as "[? ->]".

As a bonus: We also even more often write iDestruct "H" as "[? EQ]"; iDestruct "EQ" as %[= ->], i.e., there is an additional injection applied. Any way we could also get that in the proof mode? Maybe even using the "injective" typeclass so that it doesn't have to be the constructor of an inductive type (however, of course it'd also have to support all constructors, so it can't rely just on that typeclass).