proposition: Theorem evalDist_left_ident : forall rel (B : Set)(eqd : EqDec B)(b : B)(A : Set)(c2 : B -> Comp A) a, RatRel rel -> rel (evalDist (x <-$ ret b; (c2 x)) a) (evalDist (c2 b) a).
proof: Proof. intuition. eapply refl. eapply evalDist_left_ident_eq. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia Coq.Classes.RelationClasses Coq.Classes.Morphisms