A formal proof of the Chip Model Channel Separation Property

   ┌─────────┐    ┌─────────┐
───┤ pick ch ├───►┤  chip   ├──►
   └─────────┘	  └─────────┘

   ┌─────────┐    ┌─────────┐
───┤  chip   ├───►┤ pick ch ├──►
   └─────────┘	  └─────────┘