I am wondering why the tactic
apply ... with ... cannot be applied to hypotheses.
Here is an example.
Theorem in_not_nil : forall A (x : A) (l : list A), In x l -> l <> . Proof. intros A x l H. unfold not. intro Hl. destruct l eqn:HE. - simpl in H. destruct H. - discriminate Hl. Qed.
Lemma in_not_nil_42_take2_no_second_implication : forall l : list nat, In 42 l -> l <> . Proof. intros l H. apply in_not_nil with (x := 42). apply H. Qed.
apply ... with ... works well in this lemma where
l <>  is the goal.
Lemma in_not_nil_42_take2 : forall l : list nat, In 42 l -> l <>  -> true = true. Proof. intros l H1 H2. apply in_not_nil in H2 with (x := 42). apply H. Qed.
However, if we turn
l <>  into one hypothesis, it does not work.
I would like to know why it doesn’t work and how we can solve it.