fact: Definition hdisjoint (h1 h2: heap) : Prop := forall l, h1 l = None \/ h2 l = None.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)