lim*_*imp 5 coq
如果我在Coq,我发现自己处于这样一个目标:
================== x = y -> y = x
有一种策略可以一举完成吗？事实上,我正在写作
intros H. rewrite -> H. reflexivity.
但它有点笨重.
Vin*_*inz 8
要"翻转" H: x = y你可以使用的平等symmetry in H.如果你想翻转目标,只需使用symmetry.
H: x = y
symmetry in H
symmetry
归档时间：
10 年，11 月 前
查看次数：
1230 次
最近记录：