λ _ : word128 * word128,
(opp_subproof0, opp_subproof1)%core
     : word128 * word128 → word128 * word128