proposition: Lemma evalDet_repeat_steps_done_inv_h : forall (A : Set)(P : A -> bool) x y, evalDet_repeat_steps P x y -> forall c s, x = (cs_more c s) -> evalDet_steps (cs_more (Repeat c P) s) y.
proof: Proof. induction 1; intuition; subst. inversion H1; clear H1; subst. econstructor. eauto. simpl. eapply evalDet_steps_trans. eapply evalDet_steps_bind_done. eauto. rewrite H0. econstructor. eauto. simpl. econstructor. inversion H0; clear H0; subst. econstructor. eauto. simpl. eapply evalDet_bind_eof. trivial. inversion H2; clear H2; subst. econstructor. eauto. simpl. eapply evalDet_steps_trans. eapply evalDet_steps_bind_done. eauto. rewrite H0. eauto. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia