proposition: Theorem getSupport_length_nz : forall (A : Set)(c : Comp A), well_formed_comp c -> length (getSupport c) > 0.
proof: Proof. induction 1; intuition; simpl in *. apply length_getUnique_nz. apply length_nz_exists in IHwell_formed_comp. destruct IHwell_formed_comp. eapply length_flatten_nz. eapply in_map_iff. econstructor; intuition; eauto. eapply H1. trivial. apply getAllBvectors_length_nz. destruct (filter P (getSupport c)); simpl in *; intuition. Qed.
imports: Bvector List FCF.Blist FCF.EqDec FCF.Fold FCF.EqDec