# Mix

From LLWiki

The usual notion of is the binary version of the rule but a nullary version also exists.

## Binary rule

The rule is equivalent to :

They are also equivalent to the principle :

## Nullary rule

The rule is equivalent to :

The nullary acts as a unit for the binary one:

If π is a proof which uses no rule and no weakening rule, then (up to the simplification of the pattern above into nothing) π is either reduced to a rule or does not contain any rule.