proposition: Lemma evalDet_repeat_steps_nil_inv : forall (A : Set)(P : A -> bool) c a ls', evalDet_repeat_steps P (cs_more c nil) (cs_done a ls') -> ls' = nil.
proof: Proof. intuition. eapply evalDet_repeat_steps_nil_inv_h; eauto. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia