Let X, Y, f, g and W be given.
Assume Hfun: function_on f X Y.
Apply set_ext to the current goal.
Let x be given.
Assume HxL: x ∈ preimage_of X (compose_fun X f g) W.
We will prove x ∈ preimage_of X f (preimage_of Y g W).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun (compose_fun X f g) x0 ∈ W) x HxL).
We prove the intermediate claim HxW: apply_fun (compose_fun X f g) x ∈ W.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun (compose_fun X f g) x0 ∈ W) x HxL).
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 HfxY: apply_fun f x ∈ Y.
An exact proof term for the current goal is (Hfun x HxX).
We will prove x ∈ {x0 ∈ X|apply_fun f x0 ∈ preimage_of Y g W}.
We prove the intermediate claim HfxInPre: apply_fun f x ∈ preimage_of Y g W.
We will prove apply_fun f x ∈ {y ∈ Y|apply_fun g y ∈ W}.
We prove the intermediate claim HgfxW: apply_fun g (apply_fun f x) ∈ W.
rewrite the current goal using Hcomp (from right to left).
An exact proof term for the current goal is HxW.
An exact proof term for the current goal is (SepI Y (λy0 : set ⇒ apply_fun g y0 ∈ W) (apply_fun f x) HfxY HgfxW).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun f x0 ∈ preimage_of Y g W) x HxX HfxInPre).
Let x be given.
Assume HxR: x ∈ preimage_of X f (preimage_of Y g W).
We will prove x ∈ preimage_of X (compose_fun X f g) W.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun f x0 ∈ preimage_of Y g W) x HxR).
We prove the intermediate claim HfxPre: apply_fun f x ∈ preimage_of Y g W.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun f x0 ∈ preimage_of Y g W) x HxR).
We prove the intermediate claim HfxY: apply_fun f x ∈ Y.
An exact proof term for the current goal is (SepE1 Y (λy0 : set ⇒ apply_fun g y0 ∈ W) (apply_fun f x) HfxPre).
We prove the intermediate claim HgW: apply_fun g (apply_fun f x) ∈ W.
An exact proof term for the current goal is (SepE2 Y (λy0 : set ⇒ apply_fun g y0 ∈ W) (apply_fun f x) HfxPre).
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 HcompW: apply_fun (compose_fun X f g) x ∈ W.
rewrite the current goal using Hcomp (from left to right).
An exact proof term for the current goal is HgW.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun (compose_fun X f g) x0 ∈ W) x HxX HcompW).
∎