proposition: Lemma getTreeSupport_not_in : forall (A : Set)(eqd : eq_dec A)(c : Comp A)(t : DistApproxTree A) n a, dat_correct c n t -> ~In a (getSupport c) -> ~In a (getTreeSupport eqd t).
proof: Proof. intuition. eapply H0. eauto using getTreeSupport_in. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat