proposition: Theorem all_permutations_permutation : forall l1 l2 : list A, In l1 (all_permutations l2) -> Permutation l1 l2.
proof: Proof. intros l1 l2 H; apply all_permutations_aux_permutation with (n := length l2); auto. Qed.
imports: List ListAux