#Mechanized #proof of the #commutativity of #zipWith in #LiquidHaskell (continued in replies)

First, we define a type alias with a value argument (it behaves like a macro for refinement types) to describe a proof of the commutativity of some binary function "A":
```
{-@ type Commutative a A = x:a -> y:a -> {A x y == A y x} @-}
```
This says: For some value, A, and for all values x and y, passing x then y to A gives the same result as passing them in the other order.