How to define a function inductively on two arguments in Coq?
Coq's fixpoint definitions require that inductive calls receive a structurally smaller argument. Deep down, a fixpoint construct takes a single argument: there's no built-in concept of a recursive definition over two arguments. Fortunately, Coq's definition of structurally smaller includes higher-order types, which is extremely powerful.

Your two-argument fixpoint definition follows a simple pattern: either the first argument becomes smaller, or the first argument remains identical and the second argument becomes smaller. This fairly common pattern can be handled by a simple fix-in-fix.

Fixpoint pair l := fix pair1 (r : Tree) :=
  match l with
    | Tip =&gt; match r with
              | Tip =&gt; TipTip
              | Bin rl rr =&gt; TipBin rl rr
            end
    | Bin ll lr =&gt; match r with
                    | Tip =&gt; BinTip ll lr
                    | Bin rl rr =&gt; BinBin (pair1 rl) (pair lr r)
                   end
  end.


For more complex cases, or if your tastes run that way, you can use recursion closer to the way it's taught in math courses, building the fixpoint from a step computation and a separate well-foundedness argument, often using an integer measure. You can also make your definition look more like a classical program in a non-total language with a separate termination using the Program vernacular.