Let x be given.

We will prove ∃f : set → set, bij {x} 1 f.

We use (λ_ : set ⇒ 0) to witness the existential quantifier.

Apply bijI {x} 1 (λ_ ⇒ 0) to the current goal.

Let y be given.

Assume _.

We will prove 0 ∈ 1.

An exact proof term for the current goal is In_0_1.

Let y be given.

Assume Hy.

Let z be given.

Assume Hz _.

We will prove y = z.

rewrite the current goal using SingE x z Hz (from left to right).

We will prove y = x.

An exact proof term for the current goal is SingE x y Hy.

Let w be given.

Assume Hw: w ∈ 1.

We will prove ∃y ∈ {x}, 0 = w.

We use x to witness the existential quantifier.

Apply andI to the current goal.

Apply SingI to the current goal.

We will prove 0 = w.

Apply cases_1 w Hw (λw ⇒ 0 = w) to the current goal.

We will prove 0 = 0.

Use reflexivity.

∎