proof(SafeEmail): DISCHARGE combineValidValid via constructor pattern + Refl premise (#142)

## Summary

Discharge `Proven.SafeEmail.Proofs.combineValidValid` in one line by
case-splitting on the `ValidationResult` constructor and using the
`Refl` premise to bind the `isValid` field to `True`.

The OWED comment already diagnosed the blocker correctly AND suggested
the discharge — this PR just applies it.

## Discharge

\`\`\`idris
combineValidValid (MkValidationResult True _) (MkValidationResult True
_) Refl Refl = Refl
\`\`\`

The pattern \`MkValidationResult True _\` plus the \`Refl\` premise
binds the \`isValid\` field to \`True\`. With both fields True,
\`(combineResults r1 r2).isValid\` reduces to \`True && True = True\`
definitionally. Proof = \`Refl\`.

## Verification

- \`/tmp/charrefl/src/TestEmail.idr\` (isolated): Exit 0
- \`/tmp/SafeEmailMinimal.idr\` (against actual proven ValidationResult
/ combineResults): Exit 0
- Zero \`believe_me\` / \`postulate\` / \`idris_crash\`

## Local-vs-CI note

Pre-existing \`validResultIsValid\` in the same module fails to compile
locally (record-field projection through a \`public export\` top-level
constant — same blocker family as SafeCSV's \`defaultDelimiterIsComma\`
we hit in PR #137). This error does NOT reproduce in CI (PR #100 merged
green with that proof). My change is purely additive.

Refs proven#90 (Phase 3 OWED triage), proven#107 (overly-cautious OWED
meta).

## Test plan

- [x] Local isolated discharge proof: Exit 0
- [ ] CI \`idris2 --check proven.ipkg\` green
- [ ] CI test suite green

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

src/Proven/SafeEmail/Proofs.idr

@@ -103,22 +103,17 @@ validResultIsValid = Refl
                       issue.severity = Warning ->
                       (addIssue issue validResult).isValid = True
 
-||| OWED: combining two valid results yields a valid result. By the
-||| definition `combineResults r1 r2 = MkValidationResult
-||| (r1.isValid && r2.isValid) (r1.issues ++ r2.issues)`
-||| (Validation.idr L78-80), with `r1.isValid = True` and
-||| `r2.isValid = True` we get `True && True = True`. Held back by
-||| Idris2 0.8.0 not reducing the record-field projection
-||| `(MkValidationResult (r1.isValid && r2.isValid) _).isValid` to
-||| `r1.isValid && r2.isValid` by Refl when `r1`, `r2` are
-||| universally quantified (no constructor in normal form to fire
-||| the projector). Discharge by case-split on `r1`, `r2` to expose
-||| the `MkValidationResult` constructor, then `Refl` after the
-||| `True && True = True` rewrite.
+||| DISCHARGED: combining two valid results yields a valid result.
+||| The OWED comment suggested the discharge pattern: case-split on
+||| `r1`, `r2` to expose the `MkValidationResult` constructor, then
+||| pattern-match the `True` field through the premise's `Refl` to
+||| collapse `True && True` to `True` directly. Empirically verified
+||| at `/tmp/charrefl/src/TestEmail.idr`.
 public export
-0 combineValidValid : (r1, r2 : ValidationResult) ->
-                      r1.isValid = True -> r2.isValid = True ->
-                      (combineResults r1 r2).isValid = True
+combineValidValid : (r1, r2 : ValidationResult) ->
+                    r1.isValid = True -> r2.isValid = True ->
+                    (combineResults r1 r2).isValid = True
+combineValidValid (MkValidationResult True _) (MkValidationResult True _) Refl Refl = Refl
 
 --------------------------------------------------------------------------------
 -- Email Structure Properties