proposition: Lemma evalDet_sublist : forall (A : Set)(c : Comp A) a ls ls', evalDet_steps (cs_more c ls) (cs_done a ls') -> exists ls'', ls = ls'' ++ ls'.
proof: Proof. intuition. eapply evalDet_sublist_h; eauto. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia