fact: Fixpoint cmp (t u : term) : comparison := match t, u with | Var x, Var y => Nat.compare x y | Var x, _ => Lt | _, Var x => Gt | Fun f ts, Fun g us => match symb_cmp f g with | Eq => let fix cmp_terms n (ts : terms n) p (us : terms p) : comparison := match ts, us with | Vnil, Vnil => Eq | Vnil, _ => Lt | _, Vnil => Gt | Vcons t ts, Vcons u us => match cmp t u with | Eq => cmp_terms _ ts _ us | c => c end end in cmp_terms (arity f) ts (arity g) us | c => c end end.
imports: Coq(List Compare_dec) CoLoR(ATrs ListDec ListSort NatUtil VecUtil)