logic - 使用 Coq 在分离逻辑中证明堆属性（子集和相等性）

Question

我想在 coq 中证明两个引理以用于进一步的证明。我已经考虑了几个小时（> = 4小时）。我想在下面得到一些关于引理的提示或部分或完整的证明。（这些引理是关于分离逻辑的。）

Lemma imply_subset: forall (h1 h2 h: heap), 
  h_union h1 h2 = h -> disjoint h1 h2 -> h_subset h2 h.
Proof.
  Admitted.

Lemma heap_equality1: forall (h1 h2 h h11: heap),
  disjoint h1 h2 -> disjoint h11 h2 -> 
    h_union h1 h2 = h -> h_union h11 h2 = h -> h1 = h11.
Proof.
  Admitted.

下面是一些定义。

(* if heap maps a natural number (address) to
None, we say the address is not a valid address,
or it is not in the domain of the heap *)

Definition heap := nat -> option nat.

(* h1 and h2 have disjoint domain *)
Definition disjoint (h1 h2: heap) : Prop := 
  forall l, not_in_dom l h1 \/ not_in_dom l h2.

(* union of two heaps *)
Definition h_union (h1 h2: heap) : heap :=
  fun l => 
    if (in_not_in_dec l h1) then h1 l else h2 l.

(* h1 is a subset of h2 *)
Definition h_subset (h1 h2: heap) : Prop := 
  forall l n, h1 l = Some n -> h2 l = Some n.