proposition: Lemma eqb_beq_nat x y : eqb x y = beq_nat x y.
proof: Proof. eq_dec x y. rewrite <- beq_nat_ok in e. rewrite e. refl. rewrite <- beq_nat_ok in n. ded (not_true_is_false _ n). rewrite H. refl. Qed.
imports: CoLoR(LogicUtil ASubstitution FSetUtil NatUtil BoolUtil EqUtil ATrs ListUtil VecUtil) Coq(OrderedTypeEx)