Этот вопрос, вероятно, тривиален, но со вчерашнего дня я застрял в нем и не смог найти соответствующее ключевое слово для поиска.
Обратите внимание на следующее:
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 "Заменить t0 на t".
Вы знаете, как сделать эту замену?