<div dir="ltr"><div><div><div>Hello, I have something similar to the below :<br><br>```<br>open import Relation.Binary.PropositionalEquality<br><br>data A : Set where<br>  a1 : A<br>  a2 : A<br><br><br><br>fun : A → A<br>fun a1 = a2<br>fun a2 = a1<br><br>bun : A → A<br>bun a1 = a2<br>bun a2 = a1<br><br>cun : A → A<br>cun a with fun a<br>cun a | a1 = a1<br>cun a | a2 = a1<br><br>gun : (a : A) → cun a ≡ a1 → A<br>gun a c with fun a<br>gun a c | a1 with bun a<br>gun a c | a1 | a1 = a1<br>gun a c | a1 | a2 = a1<br>gun a c | a2 = a1<br><br>dun : (a : A) → cun a ≡ a1 → A<br>dun a c with bun a<br>dun a c | a1 with fun a<br>dun a c | a1 | a1 = a1<br>dun a c | a1 | a2 = a1<br>dun a c | a2 = a1<br><br>--qun : (a : A) → (c : cun a ≡ a1) → gun a c ≡ dun a c<br>--qun a c with fun a<br>--... | z = ?<br><br><br>pun : (a : A) → (c : cun a ≡ a1) → gun a c ≡ dun a c<br>pun a c with bun a<br>pun a c | a1 with fun a<br>pun a c | a1 | a1 with bun a<br>pun a c | a1 | a1 | a1 = refl<br>pun a c | a1 | a1 | a2 = refl<br>pun a c | a1 | a2 = refl<br>pun a c | a2 with fun a<br>pun a c | a2 | a1 with bun a<br>pun a c | a2 | a1 | a1 = refl<br>pun a c | a2 | a1 | a2 = refl<br>pun a c | a2 | a2 = refl<br><br>```<br><br></div>Could someone explain to me why qun returns an error?<br><br></div>In my code, I have pun in the type of the function I am working on and I also have problems with with abstraction there.<br></div><div>Given gun and dun, is there a way to simplify pun, possibly removing the second bun abstraction?<br></div><div><br> <br></div></div>