Why does `Hint Resolve X` fail, where` let: X` works?

Here is a logic puzzle about the self-referential sentences I am trying to automate in Coq. The goal is to prove P1

. I am 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 context lets : X

is just one way to make the lemma X

available to auto. As I already added HQ'1

, HQ'2

and HC

for the database hint with help Hint Resolve

, everything lets

in the above solution is redundant and the following should also work:

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

      

        
        
        
      

    

But this is not the case. What's the difference between them? Does Coq contain hypotheses in context and database clues differently?