TLC有限映射库使用疑问：合并空映射右单位律无法证明

学习《分离逻辑基础》后，我尝试用TLC的finite map为分离逻辑中的堆建模，但发现它和SLF使用的有限映射库差异很大。以下是从更大定理中提取的调试用例，展示了具体的证明失败问题：

引理证明失败示例 #

成功的左单位元引理 #

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".;

调整intros后的尝试 #

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.;

其他缺失内容 #

除了上述证明问题，TLC的有限映射库还缺少disjoint_empty_l等引理，以及SLF中提供的disjoint这类映射推理战术。

疑问 #

想请教：

• 是我对TLC库的使用方法有误？
• 还是TLC本身就没有包含SLF的全部分离逻辑相关内容？
• 作为分离逻辑的初学者，是否应该直接改用SLF库？

内容的提问来源于stack exchange，提问作者user1953221