proposition: Lemma list_permut_length_1: forall a b, list_permut (a :: nil) (b :: nil) -> a = b.
proof: Proof. intros a b; unfold list_permut, meq; intro P; generalize (P a); clear P; simpl. elim (eq_elt_dec a a). intros _; elim (eq_elt_dec b a). intros b_eq_a _; apply sym_eq; trivial. intros _ Abs; simpl in Abs; absurd (1=0); trivial; discriminate. intro; absurd (a=a); trivial. Qed.
imports: decidable_set List more_list Multiset Arith Setoid