proposition: Lemma beq_ext_symb_ok : forall f g, beq_ext_symb f g = true <-> f = g.
proof: Proof. destruct f; destruct g; simpl. rewrite beq_symb_ok. intuition. subst s0. refl. inversion H. refl. intuition. discr. intuition. discr. tauto. Qed.
imports: CoLoR(ATrs VecUtil ListUtil LogicUtil NatUtil RelUtil)