Let X be given.

We will prove ∃f : set → set, bij X X f.

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

An exact proof term for the current goal is bij_id X.

∎