Восстановление лямбд в Coq без равенства экстенсиональных функций?

Question

Я перейду к основам программного обеспечения. Есть два определения данной функции обратного списка.

Fixpoint rev (l:natlist) : natlist :=
  match l with
    | nil => nil
    | h :: t => rev t ++ [h]
  end.

и хвост-рекурсивный:

Fixpoint rev_append {X} (l1 l2 : list X) : list X :=
  match l1 with
  | [] => l2
  | x :: l1' => rev_append l1' (x :: l2)
  end.

Definition tr_rev {X} (l : list X) : list X :=
  rev_append l [].

Вот где проблема приходит. Меня просят доказать их равенство, сформулировав следующую теорему: Lemma tr_rev_correct : ∀X, @tr_rev X = @rev X.

Это создает следующее состояние доказательства:

1 subgoal
______________________________________(1/1)
forall X : Type, tr_rev = rev

Тем не менее, даже если я делаю unfoldtr_rev (и / или два других определения), я получаю что-то вроде:

1 subgoal
______________________________________(1/1)
forall X : Type, (fun l : list X => rev_append l [ ]) = rev

Но я ничего не могу сделать с этой формулировкой (кроме intro X).

То, что я хотел бы иметь это:

Lemma tr_rev_correct : forall (X : Type) (l : list X), tr_rev l = rev l.

Есть ли способ заменить первое на второе без использования функциональной расширенности? (Если я не хочу переформулировать лемму, приведенную в книге.)