proposition: Lemma rwr_list_split : forall A (R : relation A) a1 a2 l1 l2, trans_clos R a1 a2 -> rwr_list R l1 l2 -> rwr_list R (a1 :: l1) (a2 :: l2).
proof: Proof. intros A R a1 a2 l1 l2 H1 H2; apply trans_clos_is_trans with (a1 :: l2). apply rwr_list_tail; assumption. apply rwr_list_cons; assumption. Qed.
imports: Coq(Setoid Relations List Wellfounded)