Let X and y0 be given.
We will prove image_of (pair_map X {(x,x)|x ∈ X} (const_fun X y0)) X = setprod X {y0}.
Apply set_ext to the current goal.
Let p be given.
Assume Hp: p ∈ image_of (pair_map X {(x,x)|x ∈ X} (const_fun X y0)) X.
We will prove p ∈ setprod X {y0}.
Set f to be the term pair_map X {(x,x)|x ∈ X} (const_fun X y0).
We prove the intermediate claim HpRepl: p ∈ Repl X (λa ⇒ apply_fun f a).
An exact proof term for the current goal is Hp.
Apply (ReplE_impred X (λa : set ⇒ apply_fun f a) p HpRepl) to the current goal.
Let a be given.
Assume HaX: a ∈ X.
Assume Heq: p = apply_fun f a.
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim Hfa: apply_fun f a = (apply_fun {(x,x)|x ∈ X} a,apply_fun (const_fun X y0) a).
An exact proof term for the current goal is (pair_map_apply X X {y0} {(x,x)|x ∈ X} (const_fun X y0) a HaX).
We prove the intermediate claim Hid: apply_fun {(x,x)|x ∈ X} a = a.
An exact proof term for the current goal is (identity_function_apply X a HaX).
We prove the intermediate claim Hc: apply_fun (const_fun X y0) a = y0.
An exact proof term for the current goal is (const_fun_apply X y0 a HaX).
rewrite the current goal using Hfa (from left to right).
rewrite the current goal using Hid (from left to right).
rewrite the current goal using Hc (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X {y0} a y0 HaX (SingI y0)).
Let p be given.
Assume Hp: p ∈ setprod X {y0}.
We will prove p ∈ image_of (pair_map X {(x,x)|x ∈ X} (const_fun X y0)) X.
Set f to be the term pair_map X {(x,x)|x ∈ X} (const_fun X y0).
We prove the intermediate claim Hp0X: (p 0) ∈ X.
An exact proof term for the current goal is (ap0_Sigma X (λ_ : set ⇒ {y0}) p Hp).
We prove the intermediate claim Hp1Sing: (p 1) ∈ {y0}.
An exact proof term for the current goal is (ap1_Sigma X (λ_ : set ⇒ {y0}) p Hp).
We prove the intermediate claim Hp1eq: (p 1) = y0.
An exact proof term for the current goal is (singleton_elem (p 1) y0 Hp1Sing).
We prove the intermediate claim Heta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta X {y0} p Hp).
We will prove p ∈ Repl X (λa ⇒ apply_fun f a).
We prove the intermediate claim Hfp0: apply_fun f (p 0) = (apply_fun {(x,x)|x ∈ X} (p 0),apply_fun (const_fun X y0) (p 0)).
An exact proof term for the current goal is (pair_map_apply X X {y0} {(x,x)|x ∈ X} (const_fun X y0) (p 0) Hp0X).
We prove the intermediate claim Hid0: apply_fun {(x,x)|x ∈ X} (p 0) = (p 0).
An exact proof term for the current goal is (identity_function_apply X (p 0) Hp0X).
We prove the intermediate claim Hc0: apply_fun (const_fun X y0) (p 0) = y0.
An exact proof term for the current goal is (const_fun_apply X y0 (p 0) Hp0X).
We prove the intermediate claim Hfp0eq: apply_fun f (p 0) = (p 0,p 1).
rewrite the current goal using Hfp0 (from left to right).
rewrite the current goal using Hid0 (from left to right).
rewrite the current goal using Hc0 (from left to right).
rewrite the current goal using Hp1eq (from left to right).
Use reflexivity.
We prove the intermediate claim Hp_as_image: p = apply_fun f (p 0).
rewrite the current goal using Heta (from left to right) at position 1.
rewrite the current goal using Hfp0eq (from left to right).
Use reflexivity.
rewrite the current goal using Hp_as_image (from left to right).
An exact proof term for the current goal is (ReplI X (λa : set ⇒ apply_fun f a) (p 0) Hp0X).
∎