proposition: Lemma perm_in s1 s2 x : perm s1 s2 -> x \In s1 -> x \In s2.
proof: Proof. move: s1 s2; apply: perm_ind=>s1 s2. - by move=>->->. - move=>y t1 t2 -> -> H; rewrite !InE; tauto. - by move=>y z t -> ->; rewrite !InE; tauto. by move=>t _ IH1 _ IH2; move/IH1; move/IH2. Qed.
imports: mathcomp(ssreflect ssrfun seq) LemmaOverloading(rels)