proposition: Lemma dat_exists_h : forall n s (A : Set)(c : Comp A), well_formed_comp c -> exists t : DistApproxTree A, dat_correct_h c s n t.
proof: Proof. induction n; intuition. destruct (@evalDet_dec _ c s). trivial. destruct H0. exists (dat_leaf (Some x)). econstructor; eauto. exists (dat_leaf None). econstructor. intuition. eapply evalDet_done_eof_func; eauto. destruct (@evalDet_dec _ c s). trivial. destruct H0. exists (dat_leaf (Some x)). econstructor. trivial. destruct (IHn (s ++ (true :: nil)) _ c). trivial. destruct (IHn (s ++ (false :: nil)) _ c). trivial. exists (dat_internal x x0). econstructor; eauto. intuition. eapply evalDet_done_eof_func; eauto. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat