fapp :: o → o → o
lam :: o → o
subst :: o → o → o
v :: o
fapp(lam(X), Y) → subst(X, Y)
subst(v, Y) → Y
subst(lam(X), Y) → lam(X)
subst(fapp(X, Z), Y) → fapp(subst(X, Y), subst(Z, Y))