proposition: Lemma brule_preserve_vars_ok' : forall l r, brule_preserve_vars (mkRule l r) = true <-> incl (ATerm.vars r) (ATerm.vars l).
proof: Proof. unfold brule_preserve_vars. intros l r. rewrite subset_Subset. split; intros h x; simpl. rewrite !vars_equiv. intuition. rewrite <- !vars_equiv. intuition. Qed.
imports: CoLoR(LogicUtil ASubstitution FSetUtil NatUtil BoolUtil EqUtil ATrs ListUtil VecUtil) Coq(OrderedTypeEx)