proposition: Lemma evalDet_repeat_steps_done_inv : forall (A : Set)(c : Comp A)(P : A -> bool) s y, evalDet_repeat_steps P (cs_more c s) y -> evalDet_steps (cs_more (Repeat c P) s) y.
proof: Proof. intuition. eapply evalDet_repeat_steps_done_inv_h; eauto. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia