I've come to prefer one particular approach to writing out a derivation tree by hand. I used to try to draw the tree by stacking up rules with horizontal separators à la Gentzen, but I could never judge how much space I would need--I'm not accustomed to filling a page bottom to top--and one page never seemed to be enough anyway.
I've found that writing judgments top to bottom, indenting to represent nesting, is much more scalable. E.g.:
⊢ (λ f.f 1) (λ x.x) : int
⊢ (λ f.f 1) : (int → int) → int
f : int → int ⊢ f 1 : int
f : int → int ⊢ f : int → int
f : int → int ⊢ 1 : int
⊢ (λ x.x) : int → int
x : int ⊢ x : int
