proposition: Lemma beq_fun : forall f ts g us, beq (Fun f ts) (Fun g us) = beq_symb f g && beq_list beq ts us.
proof: Proof. intros. rewrite <- beq_terms. refl. Qed.
imports: CoLoR(LogicUtil BoolUtil ListUtil EqUtil ListDec NatUtil ListMax) Coq(Peano_dec)