proposition: Lemma equiv_swap : forall (A : Type) (R : relation A), forall ll, (forall s t, In (s,t) ll -> R s t) -> exists ll', (forall s t, In (s,t) ll' -> R t s) /\ map (fun st => fst st) ll = map (fun st => snd st) ll' /\ map (fun st => snd st) ll = map (fun st => fst st) ll' /\ (forall s t, In (s,t) ll <-> In (t,s) ll').
proof: Proof. intros A R ll; induction ll as [ | [s t] ll]; intro E_ll. exists (@nil (A * A)); repeat split; trivial; contradiction. destruct IHll as [ll' [E_ll' [H1 [H2 H3]]]]. intros; apply E_ll; right; trivial. exists ((t,s) :: ll'); repeat split. intros t' s' [t's'_eq_ts | t's'_in_ll']. injection t's'_eq_ts; intros; subst; apply E_ll; left; trivial. apply E_ll'; trivial. simpl; rewrite H1; trivial. simpl; rewrite H2; trivial. intros [st_eq_st | st_in_ll]. injection st_eq_st; intros; subst; left; trivial. right; rewrite <- H3; trivial. intros [ts_eq_ts | ts_in_ll]. injection ts_eq_ts; intros; subst; left; trivial. right; rewrite H3; trivial. Qed.
imports: Coq(List Relations Setoid)