Let X be given.
Assume HinfX: infinite X.
Apply (xm (∃x : set, x ∈ X)) to the current goal.
Assume Hex.
An exact proof term for the current goal is Hex.
Assume Hno: ¬ (∃x : set, x ∈ X).
We will prove ∃x : set, x ∈ X.
Apply FalseE to the current goal.
We prove the intermediate claim HXeq: X = Empty.
Apply set_ext to the current goal.
Let x be given.
Assume HxX: x ∈ X.
We will prove x ∈ Empty.
Apply FalseE to the current goal.
Apply Hno to the current goal.
We use x to witness the existential quantifier.
An exact proof term for the current goal is HxX.
Let x be given.
Assume HxE: x ∈ Empty.
We will prove x ∈ X.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE x HxE).
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 finite_Empty.
An exact proof term for the current goal is (HinfX HfinX).
∎