proposition: Lemma evalDist_ret_1 : forall (A : Set)(eqd : eq_dec A)(a1 a2 : A), a1 = a2 -> evalDist (Ret eqd a1) a2 = 1.
proof: Proof. intuition. subst. simpl. destruct (eqd a2 a2); subst; intuition. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia