proposition: Lemma in_getSupport_or_evalDist_0 : forall (A : Set)(c : Comp A) a, In a (getSupport c) \/ evalDist c a == 0.
proof: Proof. intuition. destruct (in_dec (comp_eq_dec c) a (getSupport c)); intuition. right. eapply getSupport_not_In_evalDist; intuition. Qed.
imports: Crypto FCF RndNat