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