try Program Fixpoint

hello.v

Require Export Coq.Lists.List.
Require Export Coq.Arith.Arith.
Require Import Program.Wf.

Program Fixpoint merge (x : list nat) (y : list nat) {measure (length x + length y)} : list nat :=
  match x with
  | x1 :: xs =>
    match y with
      | y1 :: ys => if x1 <? y1
        then x1::(merge xs y)
        else y1::(merge x ys)
      | _ => x
    end
  | _ => y
  end.
Next Obligation.
  apply Nat.add_le_lt_mono; auto.
Qed. 


Lemma merge_length : forall l1 , forall l2 , length (merge l1 l2 ) = length l1 + length l2.
Proof.
  induction l1.
  intros.
  intuition.

  induction l2.
  intuition.

  unfold merge.
  unfold merge_func.
  rewrite Wf.WfExtensionality.fix_sub_eq_ext; simpl; fold merge_func.
  destruct (a <? a0); simpl; f_equal.

  specialize (IHl1 (a0 :: l2)).
  intuition.

  unfold merge in IHl2.
  rewrite IHl2.
  simpl.
  auto.
Qed.