Using hypotheses / applying lemmas "up to equality"
Perennial has an iExactEq
tactic that works as follows: if your goal is G
and there is a hypothesis H: P
, you can use iExactEq "H"
and then have to prove that P = G
. This can be useful when a hypothesis is equal to the goal but they don't unify -- now you can use rewrite
and f_equiv
without having to explicitly state the equality.
Similarly one could imagine an iApplyEq
that is like iApply
but in case of unification failure requires the user to prove an equality.