proposition: Theorem not_null_cons : forall a b (l : list (A * list bool)), b <> [] -> not_null l -> not_null ((a, b) :: l).
proof: Proof. intros a b l H H0; red in |- *. intros a1; simpl in |- *; red in |- *; intros [H1| H1]; auto. case H; injection H1; auto. case (H0 a1); simpl in |- *; auto. Qed.
imports: Coq(Sorting.Permutation)