Let X and Y be given.

Assume H1: X ⊆ Y.

Set f to be the term λx ⇒ x of type set → set.

We will prove ∃f : set → set, inj X Y f.

We use f to witness the existential quantifier.

Apply injI to the current goal.

An exact proof term for the current goal is H1.

Let x be given.

Assume Hx: x ∈ X.

Let x' be given.

Assume Hx': x' ∈ X.

Assume H2: x = x'.

An exact proof term for the current goal is H2.

∎