proposition: Lemma evalDet_steps_skipn_h : forall (A : Set) a1 (x y : comp_state A), evalDet_steps x y -> forall (c : Comp A)(a2 : A) s1 s2, x = (cs_more c s1) -> y = (cs_done a2 s2) -> In a1 (getSupport c) -> (a1 = a2 \/ (exists n, n > 0 /\ s2 = skipn n s1)).
proof: Proof. induction 1; subst; intuition; subst. discriminate. inversion H; clear H; subst. inversion H0; clear H0; subst. left. eapply evalDet_step_done_val_eq; eauto. symmetry in H. edestruct (evalDet_step_more_skipn_eq c0). eauto. eauto. subst. edestruct (IHevalDet_steps). eauto. eauto. eapply Permutation_in. eapply evalDet_step_more_support_preserved. eauto. eauto. intuition. intuition. destruct H0. intuition. subst. right. case_eq (evalDet_step c (skipn x s1)); intuition; rewrite H0 in H3. edestruct (evalDet_step_done_skipn). eauto. subst. inversion H3; clear H3; subst. exists (x + x0). intuition. eapply skipn_sum. inversion H3. edestruct (evalDet_step_more_skipn). eauto. subst. edestruct (evalDet_steps_done_skipn). eauto. subst. exists (x + (x0 + x1)). intuition. rewrite skipn_sum. rewrite skipn_sum. trivial. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia