proposition: Lemma low_tree_approx_same_h : forall n (A : Set)(eqd : eq_dec A)(c : Comp A)(t : DistApproxTree A) ls, dat_correct_h c ls n t -> forall a, well_formed_comp c -> lowDistApprox_ls c a n ls (lowDistApproxFromTree eqd t a).
proof: Proof. induction 1; intuition; simpl in *. eapply evalDet_lowDistApprox_ls_done. trivial. eapply evalDet_lowDistApprox_ls_not_done. trivial. intuition. simpl in *. intuition. subst. rewrite app_nil_r in *. eauto. destruct (IHdat_correct_h1 a). trivial. destruct H3. destruct (IHdat_correct_h2 a). trivial. destruct H4. intuition. unfold lowDistApprox_ls. econstructor. econstructor. intuition. simpl. eapply rel_map_app. eapply rel_map_map. eapply rel_map_eq. eapply H5. trivial. intuition. rewrite <- app_assoc in H11. simpl in *. trivial. eapply rel_map_map. eapply rel_map_eq. eapply H3. trivial. intuition. rewrite <- app_assoc in H11. simpl in *. trivial. eapply pred_count_app; eauto. simpl. rewrite <- H8. rewrite <- H9. repeat rewrite <- ratMult_num_den. rewrite <- ratAdd_den_same. eapply eqRat_terms. repeat rewrite Nat.mul_1_r. trivial. unfold posnatMult, natToPosnat, posnatToNat. rewrite Nat.mul_comm. simpl. trivial. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat