proposition: Lemma Acc_C_step_acc_c_in_context : forall R f l, (forall s, active_in_list f l s -> Acc (C_step R) s) -> Acc (c_in_context R 0 f) l.
proof: Proof. intros R f l Acc_l. rewrite acc_filtering. rewrite <- acc_one_step_list. intros s s_in_actives; apply Acc_l. unfold active_in_list. revert s s_in_actives; clear. intros s H; rewrite <- actives_ok; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)