proposition: Lemma beq_dup_symb_ok : forall f g, beq_dup_symb f g = true <-> f = g.
proof: Proof. destruct f; destruct g; simpl; try rewrite beq_symb_ok; split_all; subst; refl || discr || inversion H; refl. Qed.
imports: CoLoR(ATrs ListUtil VecUtil LogicUtil RelUtil SN)