Controlling unification order in Coq

I have a function whose second argument depends on its first argument, like this:

Definition is_nice (f : Formula) (pf : FProof f) : bool := true.

And I have a unification goal, like this

is_nice (some_formula ?u) (some_proof ?u) =^= is_nice f pf

. which fails to unify when the unification starts from left to right, but it would be unifiable when we first unify (some_proof ?u =^= pf), infer the value for u during this unification, and then proceed to unify some_formula ?u =^= f with the knowledge of u.

How do I make Coq solve such unification problem? I have the following ideas:

1. Change is_nice so that the order of parameters is different. However, I do not know how to achieve this because of the dependency between the parameters. We would need to somehow break this dependency...

2. Change is_nice so that it uses some canonical structure trickery to reorder the unification problems. There is some trick like that described in the extended version of Gonthier's 'How to make ad hoc proof automation less ad hoc' paper, but it does not seem to be directly applicable.

3. Somehow infer ?u even before the unification of that goal starts. But again, I am not sure how.

I may use UniCoq, but it is not a requirement.

As an example, consider the following piece of code:

Inductive Formula : Set :=
| f_atomic : nat -> Formula
| f_imp : Formula -> Formula -> Formula.

Inductive FProof : Formula -> Set :=
| P1 : forall (f1 f2 : Formula), FProof (f_imp f1 (f_imp f2 f1))
| MP : forall (f1 f2 : Formula), FProof f1 -> FProof (f_imp f1 f2) -> FProof f2
.

Definition is_nice (f : Formula) (pf : FProof f) : bool := true.

Lemma impl_5_is_nice': forall (n1 : nat), is_nice _ (P1 (f_atomic (n1 + 0)) (f_atomic 5)) = true.
Proof. intros. unfold is_nice. reflexivity. Qed.


Lemma impl_3_5_is_nice: is_nice _ (P1 (f_atomic 3) (f_atomic 5) ) = true.
Proof. intros.
  Fail apply impl_5_is_nice'.
  apply (impl_5_is_nice' 3).
Qed.

The types Formula and FProof represent formulas and proofs in a deeply-embedded logic. The proof script of Lemma impl_3_5_is_nice demostrates the problem: the first apply does not go through, because the unification of f_atomic (?n1 + 0) with f_atomic 3 fails. However, when we manually compare the goal and Lemma impl_5_is_nice', we can realize that n1 has to be 3, and so we can specialize the lemma.

4. Another solution would be to inspect the goal using match goal, but then the problem is that I have quite a lot of lemmas similar impl_5_is_nice', and the tactic that would do the inspection would need to understand each one of these lemmas. Ideally, this would be unified using type classes or canonical structures, but this is really a 'backup plan'.