Let X of type set be given.
Let f of type set → (set → set → set) be given.
Let R of type set → (set → set → set) → prop be given.
We will prove R X (F X f).
Apply (H2 X f) to the current goal.
We will
prove ∀x ∈ X, R x (f x).
Let x of type set be given.
We will prove R x (f x).
An exact proof term for the current goal is (H1 x H3 R H2).
∎