proposition: Lemma heap_extensionality: forall (h1 h2: heap), (forall l, h1 l = h2 l) -> h1 = h2.
proof: Proof. intros. destruct h1 as [c1 fin1], h2 as [c2 fin2]. assert (c1 = c2) by (apply functional_extensionality; auto). subst c2. f_equal. apply proof_irrelevance. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)