proposition: Lemma beq_term_var x y : beq_term (Var x) (Var y) = eqb x y.
proof: Proof. rewrite eqb_equiv, beq_term_true_iff, eqb_true_iff. intuition. inversion H. refl. subst. refl. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)