Predicate Comparison::exprImplies

If e1 evaluates to b1 then the subexpression e2 evaluates to b2.

predicate exprImplies(Expr e1, boolean b1, Expr e2, boolean b2)