proposition: Lemma evalDet_step_done_support_singleton : forall (A : Set)(c : Comp A) a s, evalDet_step c nil = (cs_done a s) -> getSupport c = a :: nil.
proof: Proof. induction c; intuition; simpl in *. inversion H; clear H; subst. trivial. case_eq (evalDet_step c nil); intuition; rewrite H1 in H0; try discriminate. destruct n; simpl. discriminate. discriminate. discriminate. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat