proposition: Theorem cover_not_nil : forall l t, cover l t -> l <> [].
proof: Proof. intros l t H; case H; simpl in |- *; auto. intros t0; discriminate. intros l1 l2 t1 t2 t3 H0 H1; red in |- *; intros H2; absurd (length l1 = length (t1 :: t2 :: l2)); auto. rewrite H2; simpl in |- *; intros; discriminate. apply Permutation_length with (1 := H0); auto. Qed.
imports: Coq(Sorting.Permutation ArithRing)