proposition: Lemma evalDet_step_more_sublist : forall (A : Set)(c : Comp A) c' ls ls', evalDet_step c ls = (cs_more c' ls') -> exists ls'', ls = ls'' ++ ls'.
proof: Proof. induction c; intuition; simpl in *; try discriminate. case_eq (evalDet_step c ls); intuition; rewrite H1 in H0. inversion H0; clear H0; subst. destruct (evalDet_step_done_inv _ _ H1); subst; simpl in *. inversion H1; clear H1; subst. exists nil. trivial. discriminate. inversion H0; clear H0; subst. eapply IHc. eauto. case_eq (shiftOut ls n); intuition; rewrite H0 in H. destruct p. inversion H; clear H; subst. exists (Vector.to_list b). eapply shiftOut_correct_inv. trivial. discriminate. inversion H; clear H; subst. exists nil. simpl. trivial. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia