proposition: Lemma equiv_in_list_2 : forall (A : Type) (R : relation A) s ll, (forall s t, In (s,t) ll -> R s t) -> In s (map (fun st => snd st) ll) -> exists t, exists ll1, exists ll2, R t s /\ ll = ll1 ++ (t,s) :: ll2.
proof: Proof. intros A R s ll E_ll s_in_ll2; rewrite in_map_iff in s_in_ll2; destruct s_in_ll2 as [[t s'] [s'_eq_s ts_in_ll]]; simpl in s'_eq_s; subst s'; destruct (In_split _ _ ts_in_ll) as [ll1 [ll2 H]]; exists t; exists ll1; exists ll2; split; trivial. apply E_ll; trivial. Qed.
imports: Coq(List Relations Setoid)