Proofs with ∧

         -- x :: a
         -- y :: b
         (x, y)   ::   (a, b)

• In logic if you can prove a and you can prove b,

• Then you may conclude a ∧ b

• (This is called ∧I)

• The analogous programming operation is constructing a pair value