proposition: Theorem evalDet_steps_bind_eof_inv_h : forall (A : Set)(x y : comp_state A), evalDet_steps x y -> forall (B : Set)(c1 : Comp B)(c2 : B -> Comp A) s, x = (cs_more (Bind c1 c2) s) -> y = (@cs_eof A) -> evalDet_steps (cs_more c1 s) (@cs_eof B) \/ exists b s', evalDet_steps (cs_more c1 s) (cs_done b s') /\ evalDet_steps (cs_more (c2 b) s') (@cs_eof A).
proof: Proof. induction 1; intuition; subst. discriminate. inversion H1; clear H1; subst. inversion H0; clear H0; subst. case_eq (evalDet_step c1 s0); intuition; rewrite H in H2. discriminate. left. econstructor. rewrite H. eauto. econstructor. discriminate. case_eq (evalDet_step c1 s0); intuition; rewrite H0 in H. inversion H; clear H; subst. right. econstructor. econstructor. intuition. econstructor. eauto. econstructor. econstructor. eauto. trivial. discriminate. inversion H; clear H; subst. edestruct (IHevalDet_steps). simpl. rewrite H0. eauto. trivial. left. econstructor; eauto. destruct H. destruct H. intuition. right. econstructor. econstructor. intuition. econstructor; eauto. trivial. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia