Why does `Hint Resolve X` fail, where `lets : X` w

Question

Here's a logic puzzle about self-referential sentences that I'm trying to automate in Coq. The goal is to prove P1. I'm also using the LibTactics library from Software Foundations.

Require Import List.
Import ListNotations.
Require Import LibTactics. 

Inductive symbol : Type := | P | Q | P' | Q'.

Definition sentence : Type := list symbol.

Variable true : sentence -> Prop.

Variable provable : sentence -> Prop.

Hypothesis HQ'1 : forall (X : sentence), true (Q' :: X) -> ~ provable (X ++ X).
Hint Resolve HQ'1.

Hypothesis HQ'2 : forall (X : sentence), ~ provable (X ++ X) -> true (Q' :: X).
Hint Resolve HQ'2.

Hypothesis HC : forall (X : sentence), provable X -> true X.
Hint Resolve HC.

Theorem P1 : 
true [Q';Q'] /\ ~ provable [Q';Q'].

The following solution works, but seems unnecessarily long :

Theorem P1 : 
true [Q';Q'] /\ ~ provable [Q';Q'].
lets : HQ'1. lets : HQ'2. lets : HC.  
jauto. Qed.

From what I understand, adding X to the context by lets : X is just one way of making lemma X available to auto. Since I already added HQ'1, HQ'2, and HC to hint database with Hint Resolve, all the lets in the solution above are redundant, and the following should also work :

Theorem P1 : 
true [Q';Q'] /\ ~ provable [Q';Q'].
jauto. Qed.

But it does not. What's the difference between the two? Does Coq treat hypotheses in context and hint database differently?