## How or is that possible to prove or falsify `forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.` in Coq?

I want to prove or falsify forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q. in Coq. Here is my approach.

Inductive True2 : Prop :=

| One : True2

| Two : True2.

Lemma True_has_one : …