Stream: Coq users

Topic: Rewriting by an equality within a dependent term

Christopher Lam (Aug 21 2023 at 20:46):

How do I make the kernel recognize that the equality I'm trying to rewrite by is eq_refl and thus is okay to rewrite within dependent terms? In my environment I have two terms that are effectively:
H: a1 = a2
H2: H = eq_refl
and I want to rewrite by H inside of a goal that is a big dependent term.

Last updated: Oct 13 2024 at 01:02 UTC