Regarding the law of mif (aka ifte, aka soft-cut, aka logical conditional) mif (mif c t' e') t e = mif c (\x -> mif (t' x) t e) (mif e' t e) You're right of course: mode matters for the predicates that involve negation, such as mif. However, I believe that the mode is orthogonal to the discussion of the mif law. The following is a better example. Again we will be using Prolog (with the built-in soft-cut). This time, we eschew any variable binding within our conditionals, in fact, any variables at all. Truth and failure is all we need. We chose c === (true; true), t' === e' === fail, t === e === true. Thus, mif (mif c t' e') t e translates to {X =1 is there so that Prolog will print something} X = 1, (((true; true) *-> fail; fail) *-> true; true). and returns one answer, 1. mif c (\x -> mif (t' x) t e) (mif e' t e) translates to X = 1, ((true; true) *-> (fail *-> true; true) ; (fail *-> true; true)). and returns two answers, 1 and 1. Indeed, using the semantics of the soft cut, we find that the first translation reduces to X = 1, true. whereas the second one reduces to X = 1, (true; true)