Understanding TLC's finite map library

Question

I'm trying to use TLC's finite maps to model heaps in separation logic, after going through Separation Logic Foundations. It's quite different from the finite map library used there though. For example, I'm not sure why simple facts like the following cannot be proved (extracted from a bigger theorem to debug).

Lemma u_empty_l : forall A B (h:map A B),
  \{} \u h = h.
Proof.
  intros.
  apply union_empty_l. (* this works *)
Qed.

Lemma u_empty_r : forall A B (h:map A B),
  h \u \{} = h.
Proof.
  intros.
  apply union_empty_r. (* why does this fail? *)
Abort.

Errors:
In environment
A : Type
B : Type
h : map A B
Unable to unify "forall x : ?T, x \u \{} = x" with "h \u \{} = h".;

If I try to leave the forall in the goal:

Lemma u_empty_r : forall A B (h:map A B),
  h \u \{} = h.
Proof.
  intros A B.
  apply union_empty_r.
Qed.

Errors:
Applied theorem does not have enough premises.;

The library is also missing simple lemmas like disjoint_empty_l, and tactics for map reasoning (disjoint) like in SLF.

I feel like I'm missing something about how the library is supposed to be used. Or is it just that TLC doesn't contain all the separation logic stuff from SLF? As a beginner should I just stick to the SLF library?