proposition: Lemma permut_length_1: forall a b, permutation [a] [b] -> eqA a b.
proof: Proof. intros a b; unfold permutation, meq. intro P; specialize (P b); simpl in *. rewrite if_eqA_refl in *. destruct (eqA_dec a b); simpl; auto; discriminate. Qed.
imports: Lia Relations Multiset SetoidList