iRewrite: Support rewriting with Coq hypotheses
iRewrite should be able to rewrite with a Coq equality embedded into Iris. Ideally, if the embedded equality is Leibniz equality, this would work even without Proper
instances.
Cc @tslilyai
iRewrite should be able to rewrite with a Coq equality embedded into Iris. Ideally, if the embedded equality is Leibniz equality, this would work even without Proper
instances.
Cc @tslilyai