fact: Definition sepconj (P Q: assertion) : assertion := fun s h => exists h1 h2, P s h1 /\ Q s h2 /\ hdisjoint h1 h2 /\ h = hunion h1 h2.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)