proposition: Lemma perm_ind2 (P : seq A -> seq A -> Prop) : P [::] [::] -> (forall x s1 s2, perm s1 s2 -> P s1 s2 -> P (x :: s1) (x :: s2)) -> (forall x y s1 s2, perm s1 s2 -> P s1 s2 -> P (y :: x :: s1) (x :: y :: s2)) -> (forall s2 s1 s3, perm s1 s2 -> P s1 s2 -> perm s2 s3 -> P s2 s3 -> P s1 s3) -> forall s1 s2, perm s1 s2 -> P s1 s2.
proof: Proof. move=>H1 H2 H3 H4; apply: perm_ind=>s1 s2; last 1 first. - by move=>t; apply: H4. - by move=>->->. - by move=>x t1 t2 -> ->; apply: H2. move=>x y t -> ->. have R : forall t, P t t by elim=>[|e t1 IH] //; apply: H2. apply: (H4 (y :: x :: t))=>//; last by apply: H3. by apply: permutation_swap eq_refl. Qed.
imports: mathcomp(ssreflect ssrfun seq) LemmaOverloading(rels)