proposition: Lemma list_permut_length_2 : forall a1 b1 a2 b2, list_permut (a1 :: b1 :: nil) (a2 :: b2 :: nil) -> (a1=a2 /\ b1=b2) \/ (a1=b2 /\ a2=b1).
proof: Proof. intros a1 b1 a2 b2 P; elim (cons_permut_in P). intro; subst a2; left; split; trivial. apply list_permut_length_1; apply remove_context_list_permut_cons with a1; trivial. intro H; elim H; clear H. intro; subst b2; right; split; trivial. apply sym_eq; apply list_permut_length_1; apply (list_permut_remove_hd (a2 :: nil) nil P). intro; contradiction. Qed.
imports: decidable_set List more_list Multiset Arith Setoid