proposition: Lemma dat_better_bind_div2 : forall (A B : Set)(c1 : Comp B)(c2 : B -> Comp A) n t1 t2, dat_correct_bind c1 c2 n t1 -> dat_correct_bind2 c1 c2 (Nat.div2 n) t2 -> dat_better t1 t2.
proof: Proof. intuition. unfold dat_correct_bind, dat_correct_bind2 in *. destruct H. destruct H0. intuition. eapply datMap_depth_better'. eapply dat_correct_dat_better. eapply H1. eapply H. eapply div2_le. eauto. simpl. eauto. eapply Nat.le_trans. 2:{ eapply div2_ge_double. } eapply Nat.add_le_mono. auto. eapply datCorrect_datDepth. eauto. intuition. eapply dat_correct_dat_better; eauto. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat