Outline of the proof

• Base case: ps = []
  • trivial, because LHS = RHS = []
• Induction step: ps = (ch',ws):ps'
  • Two cases
    • ch' == ch : the equation reduces to
      • {p1:pick ch (chip algs state1' ps')}
=== {p2:chip algs state2' (pick ch ps')}
    • ch' /= ch : the equation reduces to
      • {pick ch (chip algs state1' ps')}
=== {chip algs state2 (pick ch ps')}