proposition: Lemma perm_nil (s : seq A) : perm [::] s <-> s = [::].
proof: Proof. split=>[H|]; last by move=>->; apply: permutation_nil. move: {1 2}[::] s H (erefl (Nil A)). apply: perm_ind=>[|s1 s2 x t1 t2 ->|s1 s2 x y t ->|s1 s2 t _ IH1 _ IH2] //. by move/IH1; move/IH2. Qed.
imports: mathcomp(ssreflect ssrfun seq) LemmaOverloading(rels)