proposition: Theorem not_null_app : forall l1 l2 : list (A * list bool), not_null l1 -> not_null l2 -> not_null (l1 ++ l2).
proof: Proof. intros l1; elim l1; simpl in |- *; auto. intros (a2, l2); case l2; auto. intros l H l0 H0 H1; case (H0 a2); simpl in |- *; auto. intros b l l0 H l3 H0 H1; apply not_null_cons; auto. red in |- *; intros H2; discriminate. apply H; auto. apply not_null_inv with (1 := H0). Qed.
imports: Coq(Sorting.Permutation)