proposition: Lemma evalDet_steps_repeat_done_inv : forall (A : Set)(P : A -> bool)(c : Comp A) s a s', evalDet_steps (cs_more (Repeat c P) s) (cs_done a s') -> evalDet_repeat_steps P (cs_more c s) (cs_done a s').
proof: Proof. intuition. eapply evalDet_steps_repeat_done_inv_h. eapply H. econstructor. trivial. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia