the context you give is ill-typed (unless `a1`

and `a2`

are definitionally equal), and the right answer might depend on how you fix it...

but regardless — you can't convince Coq that `H`

is definitionally equal to `eq_refl`

— OTOH, if `H`

appears in the goal then `rewrite H2; simpl`

could help

a1 and a2 are definitionally equal - I'm effectively trying to rewrite by something like "2 = 1 + 1"

can't you use `change`

to replace `a1`

with `a2`

then? if `H`

/`H2`

don't appear in the goal, just `clear H H2`

the syntax is `change a1 with a2`

https://coq.inria.fr/refman/proofs/writing-proofs/equality.html#coq:tacn.change

Cool, yeah that worked! Didn't realize it would be that easy. Thanks!

Christopher Lam has marked this topic as resolved.

Last updated: Jun 18 2024 at 20:02 UTC