fact: Definition triple_base (P: assertion) (c: com) (Q: assertion) : Prop := forall s h, P s h -> exists s' h', star red (c, s, h) (SKIP, s', h') /\ Q s' h'.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)