proposition: Lemma refl_trans_clos_one_step_list_refl_trans_clos : forall A R (ll : list (A * A)), (refl_trans_clos (one_step_list R) (map (@fst _ _) ll) (map (@snd _ _) ll)) <-> (forall s t, In (s,t) ll -> refl_trans_clos R s t).
proof: Proof. intros A R ll; induction ll as [ | [a b] ll]; split; intro H. intros s t st_in_nil; contradiction. left. simpl in H; rewrite refl_trans_clos_one_step_list_head_tail in H; destruct H as [H1 H2]. simpl; intros s t [st_eq_ab | st_in_ll]; [injection st_eq_ab; intros; subst; apply H1 | revert s t st_in_ll; rewrite <- IHll; assumption]. simpl; rewrite refl_trans_clos_one_step_list_head_tail; split. apply H; left; apply eq_refl. rewrite IHll; intros; apply H; intros; right; assumption. Qed.
imports: Coq(Setoid Relations List Wellfounded)