Assume Hex.

Apply Hex to the current goal.

Let b be given.

Assume Hb.

We use a to witness the existential quantifier.

We use b to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HaX.

An exact proof term for the current goal is (andEL (b ∈ X) (¬ (b = a)) Hb).

Assume Hab: a = b.

We prove the intermediate claim Hba: b = a.

We will prove b = a.

rewrite the current goal using Hab (from right to left).

Use reflexivity.

An exact proof term for the current goal is ((andER (b ∈ X) (¬ (b = a)) Hb) Hba).

Assume Hno: ¬ (∃b : set, b ∈ X ∧ ¬ (b = a)).

We will prove ∃a b : set, a ∈ X ∧ b ∈ X ∧ ¬ (a = b).

Apply FalseE to the current goal.

We prove the intermediate claim HXeq: X = {a}.

Apply set_ext to the current goal.

Let x be given.

Assume HxX: x ∈ X.

We will prove x ∈ {a}.

We prove the intermediate claim Hxeq: x = a.

Apply (xm (x = a)) to the current goal.

Assume Hxa.

An exact proof term for the current goal is Hxa.

Assume Hxna: ¬ (x = a).

Apply FalseE to the current goal.

Apply Hno to the current goal.

We use x to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HxX.

An exact proof term for the current goal is Hxna.

rewrite the current goal using Hxeq (from left to right).

An exact proof term for the current goal is (SingI a).

Let x be given.

Assume HxS: x ∈ {a}.

We will prove x ∈ X.

We prove the intermediate claim Hxeq: x = a.

An exact proof term for the current goal is (SingE a x HxS).

rewrite the current goal using Hxeq (from left to right).

An exact proof term for the current goal is HaX.

We prove the intermediate claim HfinX: finite X.

rewrite the current goal using HXeq (from left to right).

An exact proof term for the current goal is (Sing_finite a).

An exact proof term for the current goal is (HinfX HfinX).