fact: Variable Indep2 : forall s t f, defined R2 f -> R3 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)