fact: Definition LocalAssertion (p : Program) (c : Class) (m : Method) (pc : PC) (st : State.t) : option Prop := match statement_at m pc with | Some (LocalAssertion e _ _) | Some (LocalAssumption e _ _) => Some (EvalPredicate p m e st) | _ => None end.
imports: Coq(List) Coq(ListSet) Coq(FSetInterface) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers)