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