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