An exact proof term for the current goal is minus_SNoCut_eq_lem (SNoCut L R) (SNoCutP_SNo_SNoCut L R HLR) L R HLR (λq H ⇒ H).