proposition: Lemma rtred_preserve_vars : preserve_vars (red R #).
proof: Proof. unfold preserve_vars. induction 1. apply red_preserve_vars. hyp. refl. trans (vars y); hyp. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)