proposition: Lemma rwr_sub_acc_sub_acc_sub : forall R l1 l2, refl_trans_clos (one_step_list (one_step R)) l2 l1 -> (forall s, In s l1 -> Acc (one_step R) s) -> (forall s, In s l2 -> Acc (one_step R) s).
proof: Proof. assert (H : forall R l1 l2, one_step_list (one_step R) l2 l1 -> (forall s, In s l1 -> Acc (one_step R) s) -> (forall s, In s l2 -> Acc (one_step R) s)). intros R l1 l2 H; induction H; simpl. intros Hacc s [s_eq_t1 | s_in_l]. apply Acc_inv with t2; [apply Hacc; left; apply eq_refl | subst s; assumption ]. apply Hacc; right; assumption. intros Hacc s [s_eq_t | s_in_l1]. apply Hacc; left; assumption. apply IHone_step_list; [ intros; apply Hacc; right; assumption | assumption]. intros R l1 l2 K; inversion K; clear K; subst; trivial. induction H0 as [l1 l2 H1 | l1 l2 l3 H1 H2]. apply H; assumption. intro H3; apply H with l2; trivial. apply IHH2; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)