Let X and Y be given.
Assume H1.
Apply H1 to the current goal.
Let f be given.
We will
prove ∃g : set → set, bij Y X g.
We use
(inv X f) to
witness the existential quantifier.
We will
prove bij Y X (inv X f).
An
exact proof term for the current goal is
bij_inv X Y f H2.