fact: Fixpoint beq_term (t u : term) := match t, u with | Var x, Var y => beq_nat x y | Fun f ts, Fun g us => let fix beq_terms n (ts : terms n) p (us : terms p) := match ts, us with | Vnil, Vnil => true | Vcons t ts', Vcons u us' => beq_term t u && beq_terms _ ts' _ us' | _, _ => false end in beq_symb f g && beq_terms _ ts _ us | _, _ => false end.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)