Error: Cannot guess decreasing argument of fix. Coq

I have the following definition for terms :

Require Import Coq.Arith.Arith.
Require Import Coq.Lists.List.
Require Import Coq.Strings.String.
Import ListNotations.

Definition VarIndex:Type := nat.


Inductive Term : Type :=
   |Var : VarIndex -> Term
   |Comb: string   -> (list Term) -> Term.


 (*compare two list *)
Fixpoint beq_list {X:Type} (l l' :list X) (EqX :X -> X -> bool): bool :=
     match l with
       | [] => match l' with
                | []  => true
                | a   => false
              end
       | (x::xs) => 
              match l' with
                |[]      => false
                |(y::ys) => if (EqX x y) then beq_list xs ys EqX else false 
              end
     end.


Fixpoint length {X : Type} (l : list X) : nat :=
  match l with
  | nil       => 0
  | cons _ l' => S (length l')
  end. 

and a function beq_term to compare two terms define as follow :

Fixpoint beq_term (t1:Term)  (t2:Term) : bool :=
   match t1, t2 with
    | Var i, Var j             => beq_nat i j
    | Var _, Comb _ _           => false
    |Comb _ _, Var _            => false
    |(Comb s1 ts1), Comb s2 ts2 => if(beq_nat (length ts1) (length ts2)) 
                                   then beq_list ts1 ts2 beq_term
                                   else false
  end.

The definition of the function beq_term yields the error message:

Error: Cannot guess decreasing argument of fix.

So I am interested in how to convince Coq of the termination.

If you want to be able to use Coq's syntactic check in this simple example in particular, it is enough to write beq_list and beq_term into a single function.

Fixpoint beq_list (l l' :list Term) : bool :=
  match l, l' with
  | [], [] => true
  | (Var i)::xs, (Var j)::ys => beq_nat i j && beq_list xs ys
  | (Comb s1 ts1)::xs, (Comb s2 ts2)::ys => beq_list xs ys
  | _,_ => false
  end.