Alphabet

fapp:[o × o] ⟶ o
lam:[o → o] ⟶ o
h:[o] ⟶ o

Variables

X:o → o
Y:o

Rules

fapp(lam(X), Y)X · h(Y)