proposition: Lemma getTreeSupport_in : forall (A : Set)(eqd : eq_dec A)(c : Comp A)(t : DistApproxTree A) n, dat_correct c n t -> forall a, In a (getTreeSupport eqd t) -> In a (getSupport c).
proof: Proof. induction 1; intuition; simpl in *. intuition; subst. eapply getSupport_In_evalDet; eauto. intuition. unfold getTreeSupport in *. eapply in_getUnique_if in H2. simpl in *. eapply in_app_or in H2. intuition. eapply IHdat_correct_h1. eapply in_getUnique. eauto. eauto using in_getUnique. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat