这个问题可能是微不足道的，但我坚持就可以了，因为昨天我找不到相关的关键字搜索。
考虑以下：
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其持有平凡，但我不知道怎么告诉勒柯克“你的替代t0通过t ”。
你知道该怎么做替换吗？
