A coinductive calculus of binary trees