Let X be given.
We will prove function_on {(y,y)|y ∈ X} X X ∧ ∀x : set, x ∈ X → ∃y : set, y ∈ X ∧ (x,y) ∈ {(y,y)|y ∈ X}.
Apply andI to the current goal.
Let x be given.
Assume HxX: x ∈ X.
We will prove apply_fun {(y,y)|y ∈ X} x ∈ X.
rewrite the current goal using (identity_function_apply X x HxX) (from left to right).
An exact proof term for the current goal is HxX.
Let x be given.
Assume HxX: x ∈ X.
We will prove ∃y : set, y ∈ X ∧ (x,y) ∈ {(y,y)|y ∈ X}.
We use x to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HxX.
An exact proof term for the current goal is (ReplI X (λy0 : set ⇒ (y0,y0)) x HxX).
∎