proposition: Lemma getSupport_NoDup : forall (A : Set)(c : Comp A), NoDup (getSupport c).
proof: Proof. induction c; intuition; simpl in *. econstructor. apply in_nil. econstructor. eapply getUnique_NoDup. eapply getAllBvectors_NoDup. eapply filter_NoDup. trivial. Qed.
imports: Bvector List FCF.Blist FCF.EqDec FCF.Fold FCF.EqDec