proposition: Theorem not_null_map : forall (l : list (A * list bool)) b, not_null (map (fun v => match v with | (a1, b1) => (a1, b :: b1) end) l).
proof: Proof. intros l; elim l; simpl in |- *; auto. intros b; red in |- *; intros a; red in |- *; intros H; inversion H. intros (a1, l1) l0 H b; apply not_null_cons; auto. red in |- *; intros; discriminate. Qed.
imports: Coq(Sorting.Permutation)