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