Destructing term when match generates equality involving that term

Using Rocq
3

The issue with destruct (get_type f) is that Coq tries to generalize all the occurrences of get_type f before destructing it. Unfortunately, with the kind of term you are manipulating, this is usually a poor strategy, as it leads to ill-typed terms. So, you have to generalize the sub-terms manually:

Lemma untype_of_type_eq f tf: type_function f = Some tf -> untype_function tf = f.
Proof.
unfold type_function.
generalize (eq_refl (get_type f)).
generalize (get_type f) at 2 3.
now intros [t|] E [= <-].
Qed.

In particular, try to understand why eq_refl had to be generalized before get_type f.

2 Likes