proposition: Lemma pickbools_length n : pickbools n = filter (fun l => length l =? n) (pickbools n).
proof: Proof. induction n. reflexivity. simpl. rewrite filter_app. do 2 rewrite map_filter. f_equal; f_equal; f_equal. all: etransitivity; [ apply IHn | reflexivity ]. Qed.
imports: Arith ZArith String List Psatz Factorial