fact: Variable R1_reg : forall s t, R1 s t -> forall x, In x (var_list s) -> In x (var_list t) .
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)