proposition: Lemma dat_correct_bind_same: forall (A B : Set)(c1 : Comp B)(c2 : B -> Comp A) n t, well_formed_comp c1 -> dat_correct (Bind c1 c2) n t -> dat_correct_bind c1 c2 n t.
proof: Proof. intuition. unfold dat_correct_bind in *. edestruct (dat_exists). eauto. econstructor. intuition. eauto. eapply dat_correct_bind_same_h. eauto. eauto. trivial. intuition. eapply evalDet_nil; eauto. eauto. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat