proposition: Theorem evalDet_steps_done_func : forall (A : Set) x (a a' : A) s s', evalDet_steps x (cs_done a s) -> evalDet_steps x (cs_done a' s') -> (a = a' /\ s = s').
proof: Proof. intros. eapply evalDet_steps_done_func_h. eapply H. eauto. eauto. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia