fact: Variable Indep3 : forall s t f, defined R3 f -> R2 s t -> symb_in_term_list f (s :: t :: nil) = false.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)