Tac to derive contradiction from circular equality (ie. smarter to discriminate)

Question

Inductive Foo : Type :=
  | foo : Foo
  | bar : Foo -> Foo.

Lemma Foo_contr f:
  bar f = f -> False.
Proof.
  intros H.
  induction f as [|f IH].
  - discriminate.
  - injection H.
    apply IH.
Qed.

Is there a tactic which would prove Foo_circ_contr automatically? It's annoying to have to write out and prove the lemma every time, especially because AFAICT, this kind of property is true for all inductive types.

discriminate can prove that foo <> bar f, but it's not smart enough to reason about the circular equality like this.

Answer 1

The tactic to solve more complicated equality goals is called "congruence". It can solve both goals immediately:

Lemma Foo_contr f:
  bar f = f -> False.
Proof.
  induction f; congruence.
Qed.