proposition: Lemma hunion_empty: forall h, hunion hempty h = h.
proof: Proof. intros; apply heap_extensionality; intros; cbn. auto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)