proposition: Theorem evalDet_steps_bind_done : forall(A B : Set)(c1 : Comp B)(c2 : B -> Comp A) a s s', evalDet_steps (cs_more c1 s) (cs_done a s') -> evalDet_steps (cs_more (Bind c1 c2) s) (cs_more (c2 a) s').
proof: Proof. intuition. apply evalDet_steps_done_inv in H. destruct H. destruct H. intuition. eapply evalDet_steps_trans. eapply evalDet_steps_bind_more. eauto. econstructor. simpl. rewrite H1. eauto. econstructor. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia