proposition: Lemma dat_correct_dat_better : forall (A : Set)(c : Comp A) ls n1 t1, dat_correct_h c ls n1 t1 -> forall n2 t2, dat_correct_h c ls n2 t2 -> n1 >= n2 -> dat_better 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. econstructor. econstructor. specialize (H2 a). intuition. inversion H0; clear H0; subst. specialize (H a). intuition. econstructor. lia. inversion H2; clear H2; subst. specialize (H a). intuition. econstructor. assert (n >= n0). lia. eauto with dat. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat