proposition: Lemma evalDet_sublist_h : forall (A : Set)(x y : comp_state A), evalDet_steps x y -> forall (c : Comp A) a ls ls' , x = (cs_more c ls) -> y = (cs_done a ls') -> exists ls'', ls = ls'' ++ ls'.
proof: Proof. induction 1; intuition; subst; try discriminate. inversion H1; clear H1; subst. inversion H0; clear H0; subst. destruct (evalDet_step_done_inv _ _ H2). subst. simpl in *. inversion H2; clear H2; subst. exists nil. trivial. edestruct (IHevalDet_steps). symmetry. eauto. eauto. subst. symmetry in H. apply evalDet_step_more_sublist in H. destruct H. subst. exists (x0 ++ x). apply app_assoc. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia