proposition: Theorem all_in_support : forall y, In y (getSupport RndT) -> forall x, In x (getSupport RndT).
proof: Proof. intuition. eapply getSupport_In_evalDist. intuition. eapply getSupport_In_evalDist. eapply H. rewrite <- H0. eapply comp_spec_impl_eq. trivial. Qed.
imports: FCF.FCF