proposition: Theorem evalDet_steps_bind_done_inv : forall (A B : Set)(c1 : Comp B)(c2 : B -> Comp A) s s' a, evalDet_steps (cs_more (Bind c1 c2) s) (cs_done a s') -> exists b s'', evalDet_steps (cs_more c1 s) (cs_done b s'') /\ evalDet_steps (cs_more (c2 b) s'') (cs_done a s').
proof: Proof. intuition. eapply evalDet_steps_bind_done_inv_h; eauto. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia