<div dir="ltr"><div><div>Hello, <br><br></div>I have something like this : <br><br>```<br>postulate<br>  B : Set<br>  A : B → Set<br>  big_expression : {b : B} → (a : A b) → B<br>  h : {b : B} → (a : A b) → A (big_expression a)<br>  eq : {b : B} → (a : A b) → (big_expression a) ≡ b<br><br>f : {b : B} → (a : A b) → subst A (eq a) (h a) ≡ a<br>f = {!!}<br><br>```<br><br></div><div>h is defined inductively, thus it would be very easy to prove this if I did not have subst in the equality.<br><br></div><div>Any advice on how to proceed?<br><br></div><div>I can't find a way to remove subst.<br></div></div>