proposition: Theorem not_null_inv : forall (a : A * list bool) l, not_null (a :: l) -> not_null l.
proof: Proof. intros a l H; red in |- *. intros a0; red in |- *; intros H0; case (H a0); simpl in |- *; auto. Qed.
imports: Coq(Sorting.Permutation)