proposition: Lemma dat_bind_2_better : forall (n : nat) (A B : Set)(c1 : Comp B)(c2 : B -> Comp A) t1 t2, dat_correct_bind2 c1 c2 n t1 -> dat_correct_bind c1 c2 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. 4:{ eauto. } 3:{ simpl. eauto. } eapply dat_correct_dat_better; eauto. intuition. eapply dat_correct_dat_better; eauto. lia. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat