[Agda] Reasoning with Pattern Match with Default Cases

[Marco Vassena]

Suppose I have defined a function by pattern match.
In the function I am interested in one specific case, therefore I explicitly
match that one, while all the others are implicitly covered:

f : Ty -> ℕ
f Bool = 0
f τ = 0

Now I want to prove something about this function, however the
proof cannot be as concise as the definition of f:

lemma : (τ : Ty) -> f τ ≡ 0
lemma Bool = refl
lemma τ = {! refl !}  -- f τ != zero

I have to explicitly go through all the other cases, otherwise f τ won't reduce:

lemma : (τ : Ty) -> f τ ≡ 0
lemma Bool = refl
lemma Int = refl
lemma (τ => τ₁) = refl
...

As you can imagine this can be very repetitive and annoying if the proofs are more involved
and there are many values that fall in the "default" case.

Do you know if it is possible to abstract over this pattern when reasoning about
functions defined by pattern matching with a default case?

All the best,
Marco