fact: Definition triple (P: assertion) (c: com) (Q: assertion) : Prop := forall (R: assertion), independent_of R (modified_by c) -> triple_base (P ** R) c (Q ** R).
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)