问(A <-> B) -> A= B？
EN

Stack Overflow用户

提问于 2013-01-15 06:17:36

回答 1查看 138关注 0票数 1

假设我定义了这个集合。

Inductive Set_1 : Set :=
  | Constr_1 : Set_1
  | Constr_2 : Set_1.

有可能证明这一说法吗？

(Constr_1 = Constr_2) = False

如果是这样，我应该使用什么策略？这可能对autorewrite很有用。

回答已采纳

发布于 2013-01-17 21:44:49

(A <-> B) -> A = B被称为命题外延性，由classical logic隐含。

但您不需要它来使用autorewrite的等价物，只需要Require Import Coq.Setoids.Setoid即可。

票数 0

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/14327767

复制

相似问题

问(A <-> B) -> A= B？EN