proposition: Lemma brule_preserve_vars_ok : forall a : rule, brule_preserve_vars a = true <-> incl (ATerm.vars (rhs a)) (ATerm.vars (lhs a)).
proof: Proof. intro. destruct a. rewrite brule_preserve_vars_ok'. tauto. Qed.
imports: CoLoR(LogicUtil ASubstitution FSetUtil NatUtil BoolUtil EqUtil ATrs ListUtil VecUtil) Coq(OrderedTypeEx)