proposition: Lemma hunion_comm: forall h1 h2, hdisjoint h1 h2 -> hunion h2 h1 = hunion h1 h2.
proof: Proof. intros; apply heap_extensionality; intros; cbn. specialize (H l). destruct (h1 l), (h2 l); intuition congruence. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)