proposition: Lemma beq_ok : forall t u, beq t u = true <-> t = u.
proof: Proof. intro t. pattern t. apply term_ind_forall2; destruct u. simpl. rewrite beq_nat_ok. intuition. inversion H. refl. intuition; discr. intuition; discr. rewrite beq_fun. split; intro. destruct (andb_elim H0). rewrite beq_symb_ok in H1. subst f0. rewrite beq_list_ok_in in H2. subst l. refl. exact H. inversion H0. apply andb_intro. apply (beq_refl (@beq_symb_ok Sig)). ded (beq_list_ok_in H). subst v. rewrite H1. refl. Qed.
imports: CoLoR(LogicUtil BoolUtil ListUtil EqUtil ListDec NatUtil ListMax) Coq(Peano_dec)