proposition: Theorem permutation_sym : forall l m : list A, permutation l m -> permutation m l.
proof: Proof. intros l1 l2 H'; elim H'. apply permutation_nil. intros a l1' l2' H1 H2. apply permutation_skip with (1 := H2). intros a b l1'. apply permutation_swap. intros l1' l2' l3' H1 H2 H3 H4. apply permutation_trans with (1 := H4) (2 := H2). Qed.
imports: List ListAux