An exact proof term for the current goal is (λ(X Y Z : set)(H1 : X ⊆ Y)(H2 : Y ⊆ Z)(x : set)(H : x ∈ X) ⇒ (H2 x (H1 x H))).