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