The Coq manual states that the unfold qualid
tactic unfolds each occurrence of qualid
in the goal and replaces it with its beta-iota-normal form.
Is there a simple way to unfold a definition without triggering beta/iota reduction?
You might want to try e.g. the cbv
tactic like so:
Definition foo := (fun (x : nat) => x) 42.
Definition bar := (fun (x : nat) => x) 42.
Goal foo = bar.
cbv delta [foo].
This results in the following proof state:
(fun x : nat => x) 42 = bar