proposition: Lemma vmap_eqb : forall x y, VMF.eqb x y = (x =X y).
proof: Proof. intros x y; unfold VMF.eqb; unfold VMF.eq_dec. case_eq (eq_nat_dec x y); intros Hxy Hxydep. by sym; apply (proj2 (beq_nat_ok x y)). case_eq (x =X y); intros Hxyb. by elim (Hxy (proj1 (beq_nat_ok x y) Hxyb)). refl. Qed.
imports: Coq(Peano_dec Bool) CoLoR(LogicUtil EqUtil NatUtil VecUtil ATerm ASubstitution FSetUtil FMapUtil ListUtil)