The Coq mailing list

[Clément Pit-Claudel <cpitclaudel AT gmail.com>]

On 2017-10-26 10:25, Burak Ekici wrote:
> However, could not make it work whatever I did...

Does the following work for you?

  pose proof (fun x y z => eq_ind_r (fun f => f x y z = _ x y z) eq_refl H1c) 
as H';
    cbv beta in H'.

Here's a complete example:

Axiom catC: Type.
Axiom obj: Type -> Type.
Axiom arrow: forall (catC: Type), obj catC -> obj catC -> Type.
Axiom fmap : forall {C: Type} (a b: obj C), arrow C b a -> Type.
Axiom foo : forall {C a b}, arrow C b a -> arrow C b a.

Goal ((fun (a b : obj catC) (f : arrow catC b a) => fmap a b (foo f)) =
      (fun (a b : obj catC) (f : arrow catC b a) => fmap a b f) -> True).
Proof.
  intros.
  pose proof (fun x y z => eq_ind_r (fun f => f x y z = _ x y z) eq_refl H) 
as H';
    cbv beta in H'.