proposition: Theorem evalDist_left_ident_eq : forall (B : Set)(eqd : EqDec B)(b : B)(A : Set)(c2 : B -> Comp A) a, (evalDist (x <-$ ret b; (c2 x)) a) == (evalDist (c2 b) a).
proof: Proof. intuition. simpl. unfold sumList. simpl. destruct (EqDec_dec eqd b b). rewrite <- ratAdd_0_l. rewrite ratMult_1_l. intuition. congruence. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia