proposition: Theorem det_eq_impl_dist_sem_eq : forall (A : Set)(c1 c2 : Comp A), well_formed_comp c1 -> well_formed_comp c2 -> evalDet_equiv c1 c2 -> dist_sem_eq c1 c2.
proof: Proof. unfold dist_sem_eq. intuition. eapply rat_limits_eq. 2:{ eapply evalDet_evalDist_equiv. trivial. } eapply lowDistApprox_left_total. eapply comp_eq_dec; trivial. trivial. eapply limit_f_eq. eapply evalDet_evalDist_equiv. trivial. eapply evalDet_equiv_impl_lowDistApprox_equiv. eapply evalDet_equiv_symm. trivial. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat