proposition: Lemma evalDet_steps_done_evalDist_h : forall (A : Set)(x y : comp_state A), evalDet_steps x y -> forall (eqd : eq_dec A)(c : Comp A) a a' s, x = (cs_more c nil) -> y = (cs_done a s) -> well_formed_comp c -> evalDist c a' == if (eqd a a') then 1 else 0.
proof: Proof. induction 1; intuition; subst. discriminate. inversion H1; clear H1; subst. inversion H0; clear H0; subst. eapply evalDet_step_done_evalDist; eauto. assert (s = nil). eapply evalDet_step_more_nil_inv. eauto. subst. rewrite <- IHevalDet_steps; eauto. erewrite evalDet_step_nil_dist_preserved; eauto. intuition. eapply evalDet_step_well_formed_comp_preserved; eauto. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat