proposition: Lemma evalDet_step_more_skipn_eq : forall (A : Set)(c c' : Comp A)(a1 : A) s1 s2, evalDet_step c s1 = (cs_more c' s2) -> In a1 (getSupport c) -> (s1 = s2 \/ (exists n, n > 0 /\ s2 = skipn n s1)).
proof: Proof. induction c; intuition; simpl in *; try discriminate. case_eq (evalDet_step c s1); intuition; rewrite H2 in H0. inversion H0; clear H0; subst. left. eapply evalDet_step_done_ls_eq. eauto. discriminate. inversion H0; clear H0; subst. eapply in_getUnique_if in H1. apply in_flatten in H1. destruct H1. intuition. apply in_map_iff in H1. destruct H1; intuition. eapply (IHc). eauto. eauto. case_eq (shiftOut s1 n); intuition; rewrite H1 in H. destruct p. inversion H; clear H; subst. destruct n. left. rewrite shiftOut_0 in H1. inversion H1; clear H1; subst. trivial. right. exists (S n). intuition. eapply shiftOut_skipn. eauto. discriminate. inversion H; clear H; subst. intuition. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia