proposition: Lemma dat_correct_func : forall (A : Set)(c : Comp A) ls n t1, dat_correct_h c ls n t1 -> forall t2, dat_correct_h c ls n t2 -> t1 = t2.
proof: Proof. induction 1; intuition. inversion H0; clear H0; subst. assert (ca_done a = ca_done a0). eapply evalDet_func; eauto. inversion H0. subst. trivial. specialize (H1 a). intuition. specialize (H1 a). intuition. inversion H0; clear H0; subst. specialize (H a). intuition. trivial. inversion H2; clear H2; subst. specialize (H a). intuition. f_equal; eauto. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat