proposition: Lemma dat_correct_bind_same_h : forall n (A : Set)(c : Comp A) ls t, dat_correct_h c ls n t -> forall (B : Set)(c1 : Comp B)(c2 : B -> Comp A) t1, c = Bind c1 c2 -> well_formed_comp c1 -> (forall a ls', evalDet_steps (cs_more c1 ls) (cs_done a ls') -> ls' = nil) -> dat_correct_h c1 ls n t1 -> datMap_depth (fun (depth : nat) (b : B) t2 => dat_correct_h (c2 b) nil depth t2) n t1 t.
proof: Proof. induction 1; intuition; subst; simpl in *. inversion H; clear H; subst. inversion H3; clear H3; subst. inversion H; clear H; subst. apply evalDet_steps_bind_done_inv in H4. destruct H4. destruct H. intuition. econstructor. econstructor. specialize (evalDet_steps_done_func H3 H0); intuition; subst. assert (x0 = nil); eauto; subst. econstructor. eauto. apply evalDet_steps_bind_done_inv in H4. destruct H4. destruct H0. intuition. exfalso. eapply H. econstructor. eauto. apply evalDet_steps_bind_done_inv in H4. destruct H4. destruct H3. intuition. exfalso. eapply H. econstructor. eauto. inversion H3; clear H3; subst. inversion H0; clear H0; subst. econstructor. econstructor. intuition. inversion H0; clear H0; subst. assert (s' = nil); eauto; subst. eapply H. econstructor. eapply evalDet_steps_trans. eapply evalDet_steps_bind_done. eauto. eauto. econstructor. inversion H5; clear H5; subst. inversion H2; clear H2; subst. assert (s' = nil); eauto; subst. econstructor. econstructor. intuition. inversion H2; clear H2; subst. eapply H. econstructor. eapply evalDet_steps_trans. eapply evalDet_steps_bind_done. eauto. eauto. simpl. eapply dat_correct_h_bind_app; eauto. eapply dat_correct_h_bind_app; eauto. econstructor. eapply IHdat_correct_h1; eauto. intuition. eapply evalDet_app_nil; eauto. edestruct (@evalDet_dec _ c1 s); trivial. destruct H5. exfalso. eauto. eapply IHdat_correct_h2; eauto. intuition. eapply evalDet_app_nil; eauto. edestruct (@evalDet_dec _ c1 s); trivial. destruct H5. exfalso. eauto. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat