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