An exact proof term for the current goal is (λα H ⇒ andEL (TransSet α) (∀β ∈ α, TransSet β) H).