proposition: Theorem cover_all_cover_aux : forall (n : nat) l t, n = length l -> cover l t -> In t (all_cover_aux l n).
proof: Proof. intros n; elim n; simpl in |- *; auto. intros l; case l; simpl in |- *; auto. intros t H H0; inversion H0. generalize (Permutation_nil H1); intros; discriminate. intros; discriminate. intros n0 H l t H0 H1; inversion H1. simpl in |- *; auto. apply in_flat_map_in with (t1 :: t2 :: l2); auto. apply H; auto. apply eq_add_S; apply trans_equal with (1 := H0). apply trans_equal with (length (t1 :: t2 :: l2)); auto. apply Permutation_length; auto. apply permutation_all_permutations; auto. apply Permutation_sym; auto. Qed.
imports: Coq(Sorting.Permutation ArithRing)