proposition: Theorem getSupport_not_In_evalDist : forall (A : Set)(c : Comp A)(a : A), ~In a (getSupport c) <-> (evalDist c a == 0).
proof: Proof. intuition. eapply getSupport_not_In_evalDist_h. intuition. eapply getSupport_In_evalDist; eauto. Qed.
imports: FCF.Comp FCF.Rat FCF.Fold List FCF.Blist micromega.Lia FCF.StdNat FCF.NotationV1 FCF.EqDec