A formal proof of the Chip Model Channel Separation Property

Observations 2

Even if the state argument is the same on both sides of the equation we want to prove,

pick ch (chip algs state ps) === chip algs state (pick ch ps)

because of the filtering, they will be different in the recursive calls, when we try to do a proof by induction. Hence, the induction proof needs to be for a more general equation.