[Agda] Help at propositional equality proof that contains subst.

[Apostolis Xekoukoulotakis]

Hello,

I have something like this :

```
postulate
  B : Set
  A : B → Set
  big_expression : {b : B} → (a : A b) → B
  h : {b : B} → (a : A b) → A (big_expression a)
  eq : {b : B} → (a : A b) → (big_expression a) ≡ b

f : {b : B} → (a : A b) → subst A (eq a) (h a) ≡ a
f = {!!}

```

h is defined inductively, thus it would be very easy to prove this if I did
not have subst in the equality.

Any advice on how to proceed?

I can't find a way to remove subst.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170503/ed99b07e/attachment-0001.html>