proposition: Lemma evalDet_steps_done_skipn_h : forall (A : Set)(x y : comp_state A), evalDet_steps x y -> forall (c : Comp A) s a s', x = (cs_more c s) -> y = (cs_done a s') -> exists n, s' = skipn n s.
proof: Proof. induction 1; intuition; simpl in *; subst. discriminate. inversion H1; clear H1; subst. inversion H0; clear H0; subst. eapply evalDet_step_done_skipn; eauto. symmetry in H. specialize (evalDet_step_more_skipn _ _ H); intuition. destruct H0. subst. edestruct IHevalDet_steps. eauto. eauto. subst. exists (x + x0). apply skipn_sum. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia