proposition: Lemma evalDet_nil : forall (A : Set)(c : Comp A) a ls, evalDet_steps (cs_more c nil) (cs_done a ls) -> ls = nil.
proof: Proof. intuition. apply evalDet_sublist in H. destruct H. symmetry in H. apply app_eq_nil in H. intuition. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia