Let A, Y and x be given.

Assume HxY: x ∈ Y.

We will prove function_on (const_fun A x) A Y ∧ ∀a : set, a ∈ A → ∃y : set, y ∈ Y ∧ (a,y) ∈ const_fun A x.

Apply andI to the current goal.

Let a be given.

Assume HaA: a ∈ A.

We will prove apply_fun (const_fun A x) a ∈ Y.

We prove the intermediate claim Happ: apply_fun (const_fun A x) a = x.

An exact proof term for the current goal is (const_fun_apply A x a HaA).

rewrite the current goal using Happ (from left to right).

An exact proof term for the current goal is HxY.

Let a be given.

Assume HaA: a ∈ A.

We will prove ∃y : set, y ∈ Y ∧ (a,y) ∈ const_fun A x.

We use x to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HxY.

An exact proof term for the current goal is (ReplI A (λa0 : set ⇒ (a0,x)) a HaA).

∎