proposition: Lemma dat_correct_h_bind_app : forall (A B : Set) t (c1 : Comp B)(c2 : B -> Comp A) n ls1 ls2 a, evalDet_steps (cs_more c1 ls1) (cs_done a nil) -> dat_correct_h (Bind c1 c2) (ls1 ++ ls2) n t -> dat_correct_h (c2 a) ls2 n t.
proof: Proof. induction t; intuition; simpl in *. inversion H0; clear H0; subst. inversion H3; clear H3; subst. apply evalDet_steps_bind_done_inv in H1. destruct H1. destruct H0. intuition. assert (evalDet_steps (cs_more c1 (ls1 ++ ls2)) (cs_done a (nil ++ ls2))). eapply evalDet_steps_app_eq. eauto. simpl in *. specialize (evalDet_steps_done_func H1 H0); intuition; subst. econstructor. econstructor. eauto. econstructor. intuition. inversion H0; clear H0; subst. eapply H3. econstructor. eapply evalDet_steps_trans. eapply evalDet_steps_bind_done. eapply evalDet_steps_app_eq. eauto. simpl. eauto. inversion H0; clear H0; subst. econstructor. intuition. inversion H0; clear H0; subst. eapply H3. econstructor. eapply evalDet_steps_trans. eapply evalDet_steps_bind_done. eapply evalDet_steps_app_eq. eauto. simpl. eauto. eapply IHt1. eauto. rewrite app_assoc. eauto. eapply IHt2. eauto. rewrite app_assoc. eauto. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat