coq - （A <-> B）-> A = B？

Question

假设我定义了这个集合。

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

能证明这个说法吗？

(Constr_1 = Constr_2) = False

如果是这样，我使用什么策略？这可能对autorewrite.

Answer 1

(A <-> B) -> A = B称为命题外延性，由经典逻辑隐含。

但是你不需要它来使用与autorewrite,的等价物Require Import Coq.Setoids.Setoid。