1 2 3 4 5 6 7 8
foo = fun '(x, y) => x + y : nat * nat -> nat forall '(a, b), a /\ b : Prop foo = λ '(x, y), x + y : nat * nat → nat ∀ '(a, b), a ∧ b : Prop