proposition: Lemma permut_length_2 : forall a1 b1 a2 b2, permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil) -> (a1=a2) /\ (b1=b2) \/ (a1=b2) /\ (a2=b1).
proof: Proof. intros a1 b1 a2 b2 P. assert (H:=permut_cons_In P). inversion_clear H. - left; split; auto. apply permut_length_1. red; red; intros. generalize (P a); clear P; simpl. destruct (eq_dec a1 a) as [H2|H2]; destruct (eq_dec a2 a) as [H3|H3]; auto. + destruct H3; transitivity a1; auto. + destruct H2; transitivity a2; auto. - right. inversion_clear H0; [|inversion H]. split; auto. apply permut_length_1. red; red; intros. generalize (P a); clear P; simpl. destruct (eq_dec a1 a) as [H2|H2]; destruct (eq_dec b2 a) as [H3|H3]; auto. + simpl; rewrite <- plus_n_Sm; inversion 1; auto. + destruct H3; transitivity a1; auto. + destruct H2; transitivity b2; auto. Qed.
imports: Relations Setoid SetoidList List Multiset PermutSetoid Permutation