proposition: Theorem bind_low_tree_approx_same_inv : forall (A B : Set)(eqda : eq_dec A)(c1 : Comp B)(c2 : B -> Comp A) n a t r, well_formed_comp c1 -> (forall b, In b (getSupport c1) -> well_formed_comp (c2 b))-> lowDistApprox_bind c1 c2 a n r -> dat_correct_bind2 c1 c2 n t -> r == lowDistApproxFromTree eqda t a.
proof: Proof. intuition. destruct H2. intuition. inversion H1; clear H1; subst. unfold dat_correct in *. symmetry. eapply lowDistApproxFromTree_datMap_inv; intuition. eapply H4. destruct (@dat_exists n _ (c2 b)). eapply H0. eapply getTreeSupport_in. eauto. eauto. econstructor. eauto. simpl in *. eapply dat_correct_func; eauto. eapply sumList_rel_ls_intersect. eapply sumList_rel_body_eq_strong. eapply H2. intuition. erewrite H5. eapply eqRat_refl. eapply low_tree_approx_same. trivial. eapply H3. eapply low_tree_approx_same. eapply H0. eapply H1. eapply H6. intuition. eauto. eapply getSupport_NoDup. eapply getUnique_NoDup. eapply comp_eq_dec; eauto. intuition. destruct (@dat_exists n _ (c2 a0)). eapply H0. trivial. rewrite <- H5. rewrite H6. intuition. eauto. eauto. intuition. eapply ratMult_0. left. eapply getTreeSupport_approx_0. eauto. intuition. eapply ratMult_0. left. eapply getTreeSupport_approx_0. intuition. eapply H5. eapply getTreeSupport_in; eauto. Unshelve. eapply comp_eq_dec; eauto. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat