Let X, Y and Z be given.

Assume H1: Z ⊆ Y.

Let x be given.

Assume H2: x ∈ X ∖ Y.

Apply (setminusE X Y x H2) to the current goal.

Assume H3: x ∈ X.

Assume H4: x ∉ Y.

We will prove x ∈ X ∖ Z.

Apply setminusI to the current goal.

An exact proof term for the current goal is H3.

We will prove x ∉ Z.

An exact proof term for the current goal is (Subq_contra Z Y x H1 H4).

∎