postulate A : Set
postulate B : Set

-- C-c C-l: to evaluate everything
-- C-c C-,: show the current goal and the current context
-- C-c C-r: complete (or refine) the hole
-- C-c C-.: like C-c C-, but also show the type of what's written in the hole

f : A -> B -> A
f = \ (x : A) -> \ (y : B) -> x

g : A -> B -> A
g = λ (x : A) -> λ (y : B) -> x

h : A -> B -> A
h x y = x

k : A -> B -> A
k = \ x -> \ y -> x