fact: Definition EvalBinaryRefOp (op : BinaryRefOp) (r1 : option Object) (r2 : option Object) : Prop := let refEqual r1 r2 := match r1 , r2 with | None , None => True | Some l1 , Some l2 => l1 = l2 | _ , _ => False end in match op with | RefEquality => refEqual r1 r2 | RefInequality => not (refEqual r1 r2) end.
imports: Coq(List) Coq(ListSet) Coq(FSetInterface) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers)