proposition: Lemma evalDet_step_more_skipn : forall (A : Set)(c c' : Comp A) s s', evalDet_step c s = (cs_more c' s') -> exists n, s' = skipn n s.
proof: Proof. induction c; intuition; simpl in *. discriminate. case_eq (evalDet_step c s); intuition; rewrite H1 in H0. inversion H0; clear H0; subst. eapply evalDet_step_done_skipn. eauto. discriminate. inversion H0; clear H0; subst. eauto. case_eq (shiftOut s n); intuition; rewrite H0 in H. destruct p. inversion H; clear H; subst. exists n. eauto using shiftOut_skipn. discriminate. inversion H; clear H; subst. exists O. simpl. trivial. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia