proposition: Lemma hunion_assoc: forall h1 h2 h3, hunion (hunion h1 h2) h3 = hunion h1 (hunion h2 h3).
proof: Proof. intros; apply heap_extensionality; intros; cbn. destruct (h1 l); auto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)