An assumption in the goal is completely the same with a function I defined beforehand. How can I tell Coq they are indeed the same?

Question

My current goal is like this:

   1 subgoal
    fun1 : forall W : Type, list W -> list W -> list W
    H_fun1 : S_fun fun1
    V : Type
    h : V
    t : list V
    ______________________________________(1/1)
    fun2 V (fun3 fun2 V t) (h :: nil) =
    fun1 V (fun3 fun2 V t) (h :: nil)

fun2 is a function I defined before which has type forall W : Type, list W -> list W -> list W and also satisfy S_fun fun2. How can I replace fun2 by fun1 or replace fun1 by fun2 or tell Coq fun2 and fun1 are actually the same to use reflexivity to finish the proof?

Answer 1

In general, it is not possible to substitute fun2 this way, because fun1 could actually be different. However, it might be the case that the S_fun hypothesis implies that fun1 and fun2 are equal for all inputs, in which case we could conclude. Could you give us some more details about your example?