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

         -- z :: (a, b)
         fst z      ::   a
         snd z      ::   b

• In logic if you can prove a ∧ b,

• then you may conclude a

• you may also conclude b

• (These are called ∧E)

• The analogous programming operation is destructing a pair value