proposition: Lemma refl_trans_clos_one_step_list_refl_trans_clos_alt : forall A R (f g : A -> A) l, (refl_trans_clos (one_step_list R) (map f l) (map g l)) <-> (forall t, In t l -> refl_trans_clos R (f t) (g t)).
proof: Proof. intros A R f g l; induction l as [ | a l]; split; intro H. intros t t_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 t [t_eq_a | t_in_l]; [subst; apply H1 | revert t t_in_l; rewrite <- IHl; assumption]. simpl; rewrite refl_trans_clos_one_step_list_head_tail; split. apply H; left; apply eq_refl. rewrite IHl; intros; apply H; intros; right; assumption. Qed.
imports: Coq(Setoid Relations List Wellfounded)