An exact proof term for the current goal is MetaCat_struct_p_gen struct_p (λX H ⇒ H).