<div dir="ltr"><div><div><div><div>Consider this example : <br><br>```<br>module test where<br><br>open import Data.Empty<br>open import Relation.Binary.PropositionalEquality<br>open import Relation.Nullary<br><br><br>data A : Set where<br>  a1 a2 : A<br>  <br>data B : A → Set where<br>  b1 : B a1<br><br>data C : ∀{a} → B a → Set where<br>  c : ∀{a} → {b : B a} → C b<br><br>fun : ¬ (B a2)<br>fun ()<br><br><br>gun : (a : A) → (b : B a) → C b<br>gun a1 b = c<br>gun a2 b = ⊥-elim (fun b)<br><br><br>run : (a : A) → (b : B a) → gun a b ≡ c<br>run a1 b = refl<br>run a2 b = ⊥-elim (fun b)<br>```<br><br></div>For the run function, I have to provide the same proof that I gave in the gun function.<br></div>If the proof is big, then it becomes cumbersome and it increases the complexity of the code.<br><br></div>Is there a way to not do that?<br><br></div>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.</div>