proposition: Lemma dat_exists_bind2 : forall (A B : Set)(c1 : Comp B)(c2 : B -> Comp A) n, well_formed_comp c1 -> (forall b, In b (getSupport c1) -> well_formed_comp (c2 b)) -> exists t, dat_correct_bind2 c1 c2 n t.
proof: Proof. intuition. destruct (@dat_exists n _ c1). trivial. edestruct (@datMap_left_total B A (comp_eq_dec c1) x). 2:{ econstructor. econstructor. intuition. eauto. eauto. } intuition. destruct (@dat_exists n _ (c2 a)). eapply H0. eapply getTreeSupport_in. eauto. eauto. econstructor. eauto. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat