proposition: Lemma evalDet_steps_done_evalDist : forall (A : Set)(eqd : eq_dec A)(c : Comp A) a a' s, well_formed_comp c -> evalDet_steps (cs_more c nil) (cs_done a s) -> evalDist c a' == if (eqd a a') then 1 else 0.
proof: Proof. intuition. eapply evalDet_steps_done_evalDist_h; eauto. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat