proposition: Theorem getSupport_correct : forall (A : Set)(c : Comp A), Support (getSupport c)(evalDist c).
proof: Proof. intuition. econstructor. eapply getSupport_NoDup. apply getSupport_In_evalDist. Qed.
imports: FCF.Comp FCF.Rat FCF.Fold List FCF.Blist micromega.Lia FCF.StdNat FCF.NotationV1 FCF.EqDec