[Agda] merging identical proofs?

[Kenichi Asai]

I have a simple transformation that replaces all the occurrences of
0 + x in a formula with x and want to prove it correct.  The formula
is simply defined by:

data Term : Set where
  Int : N -> Term
  Add : Term -> Term -> Term

and the transformation is:

f : Term -> Term
f (Int n) = Int n
f (Add (Int 0) t1) = f t1
f (Add t t1) = Add (f t) (f t1)

When I want to prove it correct under the semantics of the formula:

interp : Term -> N
interp (Int n) = n
interp (Add t t1) = interp t + interp t1

the skeleton of the proof becomes:

correct : (t : Term) -> interp t == interp (f t)
correct (Int n) = refl
correct (Add t t1) with t
... | Int 0 = correct t1	-- interesting case
... | Int (suc n) = ?		-- uninteresting case
... | Add t2 t3 = ?		-- uninteresting case

where the proofs for the last two uninteresting cases are identical
except whether t is instantiated to Int (suc n) or App t2 t3.  My
question is: can I prove this lemma without writing the proof for
the uninteresting cases twice?

The agda file is attached.  Thank you in advance!

Sincerely,

-- 
Kenichi Asai
-------------- next part --------------
module add where

open import Data.Nat
open import Relation.Binary.PropositionalEquality
open ??Reasoning

-- Terms
data Term : Set where
  Int : ????Term
  Add : Term ??Term ??Term

-- Interpreter
interp : Term ????interp (Int n) = n
interp (Add t t?? = interp t + interp t??
-- transformation: 0 + t -> t
f : Term ??Term
f (Int n) = Int n
f (Add (Int 0) t?? = f t??f (Add t t?? = Add (f t) (f t??

-- f (0 + ((0 + 1) + 2)) = 1 + 2
ex1 : f (Add (Int 0) (Add (Add (Int 0) (Int 1)) (Int 2))) ??Add (Int 1) (Int 2)
ex1 = refl

-- Correctness
correct : (t : Term) ??interp t ??interp (f t)
correct (Int n) = refl
correct (Add t t?? with t
... | Int 0 = correct t??... | Int (suc n) = let t = Int (suc n) in
  begin
    interp t + interp t??  ??? cong (? x ??x + interp t?? (correct t) ??    interp (f t) + interp t??  ??? cong (? x ??interp (f t) + x) (correct t?? ??    interp (f t) + interp (f t??
  ??... | Add t??t??= let t = Add t??t??in
  begin
    interp t + interp t??  ??? cong (? x ??x + interp t?? (correct t) ??    interp (f t) + interp t??  ??? cong (? x ??interp (f t) + x) (correct t?? ??    interp (f t) + interp (f t??
  ??