proposition: Lemma evalDet_step_more_nil_inv : forall (A : Set)(c c' : Comp A) ls, evalDet_step c nil = (cs_more c' ls) -> ls = nil.
proof: Proof. induction c; intuition; simpl in *. discriminate. case_eq (evalDet_step c nil); intuition; rewrite H1 in H0. inversion H0; clear H0; subst. eapply evalDet_step_done_nil_inv; eauto. discriminate. inversion H0; clear H0; subst. eauto. destruct n. inversion H; clear H; subst. trivial. discriminate. inversion H; clear H; subst. trivial. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia