2 3
     : PAIR
2[+]3
     : nat
forall (A : Set) (le : A -> A -> Prop) (x y : A), le x y \/ le y x
     : Prop
match (0, 0, 0) with
| (x, y, z) => x + y + z
end
     : nat
let '(a, _, _) := (2, 3, 4) in a
     : nat