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