coq - 在证明中替换“修复”的参数

Question

这个问题可能是微不足道的，但是从昨天开始我就一直坚持下去，找不到要搜索的相关关键字。

考虑以下：

Fixpoint mfp (t: nat*nat) := fst t.

Lemma ml: forall (t: nat*nat), mfp t = fst t.
Proof.
  intros.
  unfold mfp.
  (* substitute t0 with t in lhs *)
  reflexivity.
Qed.

展开之后mfp，我必须证明(fix mfp (t0 : nat * nat) : nat := fst t0) t = fst t哪个微不足道，但我不知道如何告诉 Coq “做 by 的替换t0” t。

你知道怎么做那个替换吗？

标签： coqcoq-tactic