Let y be given.

Assume Hy: y ∈ image_of (compose_fun X f g) U.

We will prove y ∈ image_of g (image_of f U).

Apply (ReplE_impred U (λx : set ⇒ apply_fun (compose_fun X f g) x) y Hy) to the current goal.

Let x be given.

Assume HxU: x ∈ U.

Assume Hyx: y = apply_fun (compose_fun X f g) x.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (HUX x HxU).

We prove the intermediate claim Hcomp: apply_fun (compose_fun X f g) x = apply_fun g (apply_fun f x).

An exact proof term for the current goal is (compose_fun_apply X f g x HxX).

We prove the intermediate claim Hycomp: y = apply_fun g (apply_fun f x).

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

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

Use reflexivity.

We prove the intermediate claim HfxIm: apply_fun f x ∈ image_of f U.

An exact proof term for the current goal is (ReplI U (λx0 : set ⇒ apply_fun f x0) x HxU).

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

An exact proof term for the current goal is (ReplI (image_of f U) (λu : set ⇒ apply_fun g u) (apply_fun f x) HfxIm).

Let y be given.

Assume Hy: y ∈ image_of g (image_of f U).

We will prove y ∈ image_of (compose_fun X f g) U.

Apply (ReplE_impred (image_of f U) (λu : set ⇒ apply_fun g u) y Hy) to the current goal.

Let u be given.

Assume Hu: u ∈ image_of f U.

Assume Hyu: y = apply_fun g u.

Apply (ReplE_impred U (λx : set ⇒ apply_fun f x) u Hu) to the current goal.

Let x be given.

Assume HxU: x ∈ U.

Assume Hux: u = apply_fun f x.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (HUX x HxU).

We prove the intermediate claim Hcomp: apply_fun (compose_fun X f g) x = apply_fun g (apply_fun f x).

An exact proof term for the current goal is (compose_fun_apply X f g x HxX).

We prove the intermediate claim Hycomp: y = apply_fun (compose_fun X f g) x.

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

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

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

Use reflexivity.

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

An exact proof term for the current goal is (ReplI U (λx0 : set ⇒ apply_fun (compose_fun X f g) x0) x HxU).