proposition: Lemma rwr_list_cons : forall A (R : relation A) a1 a2 l, trans_clos R a1 a2 -> rwr_list R (a1 :: l) (a2 :: l).
proof: Proof. intros A R a1 a2 l H; induction H as [a1 a2 H | a1 a2 a3 H1 H2]. do 2 left; assumption. right with (a2 :: l); trivial. left; assumption. Qed.
imports: Coq(Setoid Relations List Wellfounded)