proposition: Lemma evalDet_repeat_steps_more_inv : forall (A : Set) x (c : Comp A)(P : A -> bool) s, evalDet_repeat_steps P x (cs_more c s) -> False.
proof: Proof. intuition. eapply evalDet_repeat_steps_more_inv_h; eauto. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia