proposition: Lemma beq_term_ok : forall t u, beq_term 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. apply args_eq. ded (beq_vec_ok_in1 H H2). rewrite <- H1. rewrite Vcast_refl. refl. inversion H0 as [[h0 h1]]. clear h1. subst f0. simpl. apply andb_intro. apply (beq_refl (@beq_symb_ok Sig)). apply beq_vec_ok_in2. exact H. refl. Qed.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)