Cannot Unify two hypotheses which are identical

Question

I have two hypotheses in context, but when I try to apply one to another, I get the error unable to unify. I should be able to unify them. The two hypotheses are as follo

IHl : forallb func l = true -> All (fun x : X => func x = true) l H1 : All (fun x : X => func x = true) l

My goal is to get the premise from IHl by applying IHl to H1.

Answer 1

This is a common confusion among beginners. When used on a hypothesis, the apply tactic works as follows: if H1 : A -> B and H2 : A, apply H1 in H2 replaces H2 by H2 : B. Thus, for your proof to succeed, you would have to have the reverse implication IHl : All ... l -> forallb func l = true in the context, or the hypothesis H1 : forallb func l = true.