An exact proof term for the current goal is set_ext alpha beta (tagged_eqE_Subq alpha beta Ha He) (tagged_eqE_Subq beta alpha Hb (λq ⇒ He (λu v ⇒ q v u))).