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。