proposition: Theorem getSupport_not_In_evalDist_h : forall (A : Set)(c : Comp A)(a : A), ~In a (getSupport c) -> (evalDist c a == 0).
proof: Proof. induction c; intuition; simpl in *. intuition. destruct (e a a0); subst; intuition. eapply sumList_0. intuition. eapply ratMult_0. right. eapply H. intuition. eapply H0. eapply (in_getUnique (flatten (map (fun b : B => getSupport (c0 b)) (getSupport c)))). eapply in_flatten. exists (getSupport (c0 a0)). intuition. eapply in_map_iff. exists a0. intuition. exfalso. eapply H. eapply in_getAllBvectors. apply filter_not_In in H. intuition. eapply ratMult_0. right. eauto. eapply ratMult_0. left. unfold indicator. rewrite H0. rewrite ratMult_0_l. intuition. Qed.
imports: FCF.Comp FCF.Rat FCF.Fold List FCF.Blist micromega.Lia FCF.StdNat FCF.NotationV1 FCF.EqDec