proposition: Lemma evalDet_steps_repeat_eof_inv_h : forall (A : Set)(x y : comp_state A), evalDet_steps x y -> forall (P : A -> bool)(c : Comp A) s, evalDet_steps x (cs_more (Repeat c P) s) -> y = (cs_eof A) -> evalDet_repeat_steps P (cs_more c s) (cs_eof A).
proof: Proof. induction 1; intuition; subst. inversion H. inversion H1; clear H1; subst. simpl in *. eapply evalDet_steps_bind_eof_inv in H0. intuition. econstructor. trivial. destruct H. destruct H. intuition. case_eq (P x); intuition; rewrite H in H1. inversion H1; clear H1; subst. simpl in *. inversion H6. eapply evalDet_repeat_steps_step. eauto. trivial. eapply IHevalDet_steps. eapply evalDet_steps_trans. eapply evalDet_steps_bind_done. eauto. rewrite H. econstructor. trivial. eauto. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia