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