[Agda] ⊥-elim and proof duplication. Is there another way?

[Apostolis Xekoukoulotakis]

Consider this example :

```
module test where

open import Data.Empty
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary


data A : Set where
  a1 a2 : A

data B : A → Set where
  b1 : B a1

data C : ∀{a} → B a → Set where
  c : ∀{a} → {b : B a} → C b

fun : ¬ (B a2)
fun ()


gun : (a : A) → (b : B a) → C b
gun a1 b = c
gun a2 b = ⊥-elim (fun b)


run : (a : A) → (b : B a) → gun a b ≡ c
run a1 b = refl
run a2 b = ⊥-elim (fun b)
```

For the run function, I have to provide the same proof that I gave in the
gun function.
If the proof is big, then it becomes cumbersome and it increases the
complexity of the code.

Is there a way to not do that?

Keep in mind that in this example, we could avoid ⊥-elim, we could simply
case split on b. I am referring to the cases where we cannot avoid ⊥-elim.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170718/0b28c8b9/attachment.html>