proposition: Lemma rwr_list_tail : forall A (R : relation A) a l1 l2, rwr_list R l1 l2 -> rwr_list R (a :: l1) (a :: l2).
proof: Proof. intros A R a l1 l2 H; induction H as [l1 l2 H | l1 l2 l3 H1 H2]. left; right; assumption. right with (a :: l2); trivial. right; assumption. Qed.
imports: Coq(Setoid Relations List Wellfounded)