proposition: Lemma evalDet_steps_done_skipn : forall (A : Set)(c : Comp A) s a s', evalDet_steps (cs_more c s) (cs_done a s') -> exists n, s' = skipn n s.
proof: Proof. intuition. eapply evalDet_steps_done_skipn_h; eauto. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia