Let X, f, V and W be given.

Assume HVW: V ⊆ W.

Let x be given.

Assume Hx: x ∈ preimage_of X f V.

We will prove x ∈ preimage_of X f 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 ∈ V) x Hx).

We prove the intermediate claim HfxV: apply_fun f x ∈ V.

An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun f x0 ∈ V) x Hx).

We prove the intermediate claim HfxW: apply_fun f x ∈ W.

An exact proof term for the current goal is (HVW (apply_fun f x) HfxV).

An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun f x0 ∈ W) x HxX HfxW).

∎