fact: Definition pureconj (P: simple_assertion) (Q: assertion) : assertion := fun s h => P s /\ Q s h.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)